Ide_intf.to_answer: dynamically check that answer & call correspond

 Without this, it was probably possible to crash Coqide by forging
 inadequate answers to a call. Backport of trunk commits 15983-15985.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15987 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixed bug #2930: folded let-in's were hiding a violation to the occur
check condition in pattern-unification, resulting in the instantiation
of evars by terms depending on themselves, henceforth leading
eventually to a stack overflow. Occur-check in the arguments of evars
was also missing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15997 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: better handling of gtk messages + fix win32 stdout/stderr rerouting

 We now try harder to handle ourselves gtk messages (e.g. Gtk-WARNING ...).
 This way, we could reroute them nicely in w32, and pop-up the critical ones.

 Moreover, the code rerouting debug messages to a log file in w32 was using
 !Ideutils.debug before its initialization. Now, when a log file is used, its
 name is displayed in the about messages.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16012 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: better removal of the error red tag

 Instead of trying to limit the retag to the visible zone
 (which may be wrong if the user has scrolled), we remove
 the red error tag from the whole buffer (this isn't costly).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16013 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: simplify tag_on_insert, no potentially invalid iters in a callback

 Do not try to delay the retag of the rest of the buffer in case
 the small local retag raises Unterminated. This delayed callback
 was posing synchronicity issues, moreover the direct use of iters
 in it was *wrong*, these iters could have become invalid meanwhile.

 Instead, we retag the rest immediatly if necessary, this isn't that
 time-consuming anyway (linear pass on the buffer).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16014 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqmktop: a Filename.quote was blocking the removal of temp files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16015 85f007b7-540e-0410-9357-904b9bb8a0f7
Correction des entêtes pour la documentation en ligne

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16062 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction of projections: restrict a hack to ocaml only (fix #2941)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16075 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixed a bug in the algorithm elaborating a "match" return predicate.

This occurred in a second choice strategy which is anyway probably not
used in general, but the bug showed up in error messages since these
messages reports on the second choice when the first choice has failed
because of user-side typing error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16079 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Do not display REVERTcast inserted by reduction tactics (unless
printing all). Question of printing DEFAULTcast inserted by reduction
tactics still open.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16082 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixed interpretation of "x" as a binding variable for the return
predicate in "match x return ... with" when x is a goal variable.
Commit 4926 forbade it but too strongly. AFAICS, only notation
variables have to be avoided.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16084 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixed a little inefficiency of "set/destruct" over a pattern. Now
different instances of a meta are checked against full conversion.

Note: This backports the combination of the last two previous trunk commits.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16087 85f007b7-540e-0410-9357-904b9bb8a0f7
No more constant named "int" in Coq theories (cf bug #2878)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16090 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction: qualified names in Extract Constant examples (fix #2878)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16091 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Taking into account the possibility of having a type of type which is
an evar in typing.ml. Thanks to HoTT people for noticing the problem.

Fixed behavior of e_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16093 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing parsing of specific primitive tokens used as notations
for patterns (e.g. 1 for eq_refl). Fixing printing of notations that
are not just abbreviations for constructors with no arguments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implementing the "union by rank" optimisation in univ.ml
* Bugfixes in union by rank in univ.ml
* kernel/univ.ml: clarify the rank union selection logic

Author: Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>
Author: Gabriel Scherer <gabriel.scherer@inria.fr>

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16096 85f007b7-540e-0410-9357-904b9bb8a0f7
Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)

 Inner sub-modules with "Definition t := t" is hard to handle by
 extraction: "type t = t" is recursive by default in OCaml, and
 the aliased t cannot easily be fully qualified if it comes from
 a higher unterminated module. There already exists some workarounds
 (generating Coq__XXX modules), but this isn't playing nicely with
 module types, where it's hard to insert code without breaking
 subtyping.

 To avoid falling too often in this situation, I've reorganized:

 - GenericMinMax : we do not try anymore to deduce facts about
   min by saying "min is a max on the reversed order". This hack
   was anyway not so nice, some code was duplicated nonetheless
   (at least statements), and the module structure was complex.

 - OrdersTac : by splitting the functor argument in two
   (EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid
   the need for aliasing the type t, cf NZOrder.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16101 85f007b7-540e-0410-9357-904b9bb8a0f7
update CHANGES for 8.4pl1

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16108 85f007b7-540e-0410-9357-904b9bb8a0f7
Hashtbl_alt: bug spotted by Enrico

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