make validate repaired via a temporary fix for #2949

 I simply provide an explicit argument to one of the functors, avoiding
 the faulty use of the "include-to-self" feature there.
 Note that this NZOrderedType functor could also be simply removed
 as in trunk, since it isn't used anywhere.

 Btw, the Not_found in coqchk is now turned into something slightly
 more informative.

 The core of the bug remains: coqtop should check that "include-to-self"
 hasn't produced a chimera (more details in the bug tracker).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16201 85f007b7-540e-0410-9357-904b9bb8a0f7
Corrects bug #2959 (error during Qed leads to assertion failure).

Well-placed [Proof.transaction]-s do the trick.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16226 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: A slightly more efficient test of well-typedness of restriction of
evars (though this might be slighty more costly).

This incidentally solves Appel's part of bug #2830 even though a
conceptual problem around the interaction of unification with the
proof engine has to be solved. Indeed, what to do when unification,
called as part of a tactic, solves or refines the current goal by side
effect. Somehow, unifyTerms or tclEVARS should take this possibility
into consideration, either by forbidding the refinement of the current
goal by side effect, or by acknowledging this refinement by producing
new subgoals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16233 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Added missing documentation of Set Printing Existential Instances.

Also started a preliminary documentation about evars (where to have it
in the doc is somehow open).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16235 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix compilation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16242 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing bug #2466

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16246 85f007b7-540e-0410-9357-904b9bb8a0f7
Restrict try...with to avoid interfering with Sys.Break

 This is a restricted version of the patchs applied recently on
 trunk. Idea: catching-all try...with are now restricted via
 a "when Errors.noncritical e" clause. In the 8.4 branch, this
 Errors.noncritical function only excludes the Sys.Break (and
 Out_ot_memory and Stack_overflow), but not the anomalies, for
 maximal compatibility.

 This commit concerns only coqtop and its plugins
 (no checker / ide / tools).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16313 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction AccessOpaque is now activated again by default (fix #2952)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16316 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix for bug #3004 (thanks Hugo !)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16318 85f007b7-540e-0410-9357-904b9bb8a0f7
A few optimizations around kernel_names...

 For instance, let's avoid computing twice subst_mp when possible.
 Interest: small speed-up, but also improved sharing of results,
 hence slightly smaller vo.

 Inspired by changes already done in trunk, but I won't backport
 to 8.4 the more radical changes done recently (pairs of kernel_names
 not coded as pairs anymore when possible).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16319 85f007b7-540e-0410-9357-904b9bb8a0f7
Reworked interrupt mechanism for w32 (should fix #2869)

 There were problems with the Stop button after a Restart button.
 This seems related with the way the Consoles were handled between
 coqide and the coqtop clients (the stdout/stderr redirections were
 also probably concerned).

 So here is now a simpler mechanism that seems to work fine:

 - Coqide is again an app *with* console (but we hide this console
   asap at launch-time, unless in debug mode)

 - This console is shared with the different coqtop clients
   (Cf. win_create_process_native in ocaml's
   otherlibs/win32unix/createprocess.c)

 - The Stop button sends a Ctrl-C event to *all* the clients.
   This shouldn't be an issue since at most one of the coqtops
   is busy at a given time. At worst there will be spurious
   "Interrupted" messages in the other tabs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16324 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide w32 : a forgotten line in previous commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16325 85f007b7-540e-0410-9357-904b9bb8a0f7
Check a list length before doing a List.chop (fix #3000)

 I'm not completely sure that raising Not_found is the right
 thing to do here, but it seems reasonable...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16327 85f007b7-540e-0410-9357-904b9bb8a0f7
Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16330 85f007b7-540e-0410-9357-904b9bb8a0f7
Printmod: handle more examples thanks to better nametab use

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16331 85f007b7-540e-0410-9357-904b9bb8a0f7
Check unexpected "Local" keyword in cmd before opening a proof (fix #2975)

 This fix isn't ideal. Instead, something like States.with_heavy_rollback
 should be able to cancel a proof started during a command interp that failed.
 But anyway, "le mieux est l'ennemi du bien"...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16334 85f007b7-540e-0410-9357-904b9bb8a0f7
Firstorder: record with defined field aren't conjonctions (fix #2629)

 The let-in in the type of constructor was perturbating the
 Hipattern.dependent check, leading firstorder to consider too much
 inductives as dependent-free conjonctions, ending with lift errors
 (UNBOUND_REL_-2, ouch).

 This patch is probably overly cautious : if the variable of the
 let-in is used, we consider the constructor to be dependent.
 If someday somebody feels it necessary, he/she could try to reduce
 the let-in's instead...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16340 85f007b7-540e-0410-9357-904b9bb8a0f7
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)

 Since the nametab isn't aware of everything needed to print mismatched
 types (cf the bug test-cases), we create a robust term printer that
 known how to print a fully-qualified name when [shortest_qualid_of_global]
 has failed. These Printer.safe_pr_constr and alii are meant to never fail
 (at worse they display "??", for instance when the env isn't rich enough).

 Moreover, the environnement may have changed between the raise
 of NotConvertibleTypeField and its display, so we store the original
 env in the exception.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16343 85f007b7-540e-0410-9357-904b9bb8a0f7
Restore final line break when printing 0 or >= 2 goals in coqtop (was
removed in r15592 and r15511). I hope this doesn't break some other
non-coqtop uses of coq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16345 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing unfolding of local definitions during unification that appeared
with commit r16233. This commit added a more precise filtering of
variables on which an evar was allowed to be dependent, but) but it
also broke some Ssreflect scripts. The reason why that filtering was
incorrectly applied, sometimes, to local definitions;

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16347 85f007b7-540e-0410-9357-904b9bb8a0f7