Do not overallocate closures' named environments in infos. Modifying the access
function is sufficient to skip the undefined variables.
Dedicated inductive for return values of rewrite strategies.
Added test-suite for bug #2990.
A few fixes to the build system (mostly for ocamlbuild)

 * vars.mli was mentionning Term instead of Constr, leading to a dep cycle
 * Having a file named toplevel/toplevel.ml isn't a good idea when we also
   have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
   We rename toplevel.ml into Coqloop.ml
 * Extra cleanup of toplevel.mllib :
   - Ppextra isn't anywhere around (?!)
   - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
   - Vernacexpr is a .mli and shouldn't appear in an .mllib
 * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
 * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
   for coqchk).
Get rid of messages "emitting ..." when compiling .v files

 If these messages are still relevent to somebody, feel free to
 restore them in -debug or any non-default mode of your choice.
Removing the need of evarmaps in constr internalization.

Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
Tentative fix of the guardedness checker by Christine and me. All stdlib and test-suite pass.
Merge branch 'trunk' of github.com:coq/coq into trunk
Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4e

Attempt to adapt .el files too.
doc/refman/RefMan-uti.tex has still to be fixed.
test guard condition against feature incompatible with prop-ext
Missing Fail in r16792
Printing function for Stdargs in debugger
Bad use of Obj.magic in interpretation of TacAlias arguments.
It triggered nonsensical behaviour of list-using tactic
notation. Hopefully or not, nobody uses such notations out of
the test-suite...
test-suite/output/Notations : evar number change
Using interp_genarg in tactic notations where possible, instead of an ad-hoc
interpreter.
Removing the useless pattern ident genarg.
micromega: removal of spurious Export; addition of Lia.v encapsulating lia and nia.
Coqdep always uses / as dir_sep
List: Bug 3039 weaker requirement for fold symmetric
Warning removal