In discrimination nets, do not index lambdas if they're part of a beta
redex.
Two fixes in unification (bugs #3782 and #3709)
- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.
Searchxxx now search also the hypothesis and support goal selector.

Documentation also updated.
Extend the syntax of simpl with a delta flag.

You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
An option SimplIsCbn
Fix #3800 : cmxs need execution priviledges under windows
Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll"
#4843 part 2 : The .cmxs files for plug-ins must have execute permission
Searchxxx now interpret patterns in goal environment if any.

This makes such things work:

x:nat
h: x = 3
================
True

Search x.
Make sure the goals on the shelve are identified as goal and unresolvable for typeclasses.

This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.

Fixes #3841.
Add Ltac syntax for the [tclIFCATCH] primitive.

[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
Revert "Fixing bug #3817."

This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
Fixing bug #3858 and #3817 in one stroke.
Fix merging of name maps in union of universe contexts.
Util.un_op -> Option.default
Fixing bug #3865.
Tests for Searchxxx commands added and modified.
Fix treatment of universe context in typecheck inductive (was added
twice). Thanks to Marc Lasson for spotting this.
About now accepts hypothesis names and goal selector.
Documenting check_record + changing a possibly undefined int into int option.