Fix the refine related test-suite files to account for the new refine.
Remove duplicate test-suite file.

success/instantiate.v was a duplicate of bugs/closed/1041.v
Fix test-suite/success/evars.v.

In commit a92a27 (Fix the compilation of pattern matching wrt to variables), I introduced a serious bug in which, in some case, the infered return predicate of a pattern matching would be lifted wrongly. Because I wrote [false] instead of [true] at one location (which prevented creation of aliases and so created shorter named_context than expected).
Stylistic change.

I doubt [catching_error] is performance critical in any way. But it looked silly to allocate a block to [(inner_trace,e)] when [e] was known in advance (and was already named [e]).
Fix printing of Ltac's backtrace.

I used an exception wrapper to report Tactic failures. It had the consequence of making process_vernac_interp_error to look for the backtrace at the wrong place.
Renaming elisp files to avoid conflict with pg in distribs.
Fix CoqIDE on windows
Fixing backtrace registering of various tactic-related try-with blocks.
Fix CoqIDE compilation under standard version of lablgtk2

We use the win32 specific function only if WIN32 is defined
Documenting the tactic-in-term construction.
Generalize eq_proofs_unicity

The generalizded version is eq_proofs_unicity_one_var. We preserve
backwards compatibility, unless someone used nu_left_inv (which was
defined as a Remark(!), but whose type depended on a number of Lets.)

We could keep going in defining one variable variants, but I was lazy.
I'm also not sure if we should be breaking backward compatiblity to
generalize these theorems, if we should make separate files for the
pointed versions, or if we should just have duplicate theorems in each
file.  (I'm also not sure if I should call it _one_var or _pointed or
something else.)

This closes Bug 3019.
Better unification for [projT1] and [proj1_sig].

This way, [fun A (P : A -> Prop) (X : sigT P) => proj1_sig X] unifies
with [fun A (P : A -> Prop) (X : sigT P) => projT1 X].

This closes Bug 3043.
Patch for supporting [From Xxx Require Yyy Zzz.]

When using libraries I find it convenient (and future proof) to use fully qualified paths in many places. It would be nice to have a convenient short-hand for this so that you can:

From Xxx Require Yyy Zzz.

instead of having to type:

Require Xxx.Yyy Xxx.Zzz.

Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
Do not compile coqide with -thread

Coqide compiled with -thread seems to hang for ever at startup under MacOS
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.