v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16183 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing coqchk compilation after commit r16183

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16184 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixed bug #2981 (anomaly NotASort in Retyping due to collision between
variable names).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16185 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "Ordered evars by level of dependency in the merging phase of unification"

Though this commit provides with more "natural" instances of metas
found by unification, it breaks a few contribs. The best approach to
try is maybe now to instead plug apply on evarconv.ml, rather than on
unification.ml!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16191 85f007b7-540e-0410-9357-904b9bb8a0f7
Moved code from Pretype_error to Evarutil

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16194 85f007b7-540e-0410-9357-904b9bb8a0f7
Splitted Evarutil in two files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16195 85f007b7-540e-0410-9357-904b9bb8a0f7
Useless use of hooks in VernacDefinition. In addition, this was
polluting the AST first-order structure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16196 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing bug in native compiler with let patterns in fixpoint definitions.
Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n.
Was raising an "index out of bounds" exception at compile-time.
Nota: this construction is still incorrectly handled by the VM.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7
Checker: re-sync vo structures after Maxime's commit 16136

 make validate still fails, but that's another issue (#2949) we're
 still working on...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16198 85f007b7-540e-0410-9357-904b9bb8a0f7
make validate repaired via a temporary fix for #2949

 The offending functor in NZOrder wasn't actually used, so
 I've commented it for now.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing autocompletion lock in CoqIDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16200 85f007b7-540e-0410-9357-904b9bb8a0f7
CoqIDE: Adding escape reaction to replace widget

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16202 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix extraction of inductive types that Coq auto-detects to be in Prop

 Typical example :

   Inductive t := T : t -> t.

 Earlier, the extraction was using a shortcut to get the sort of t
 (via some mind_arity stuff), but this was producing a less precise
 answer (here InType) than a full Retyping.get_sort_family_of
 (here InProp since t is a singleton type, with no content).
 The extraction of t was hence awkward, since the type of the
 constructor T was computed with the precise method, and its argument
 was optimized out. Now the whole t is considered logical by the
 extraction.

 NB: to avoid this clever but highly non-intuitive behavior of Coq placing
 the above t in Prop, for the moment you have to fix its sort, for instance:

  Inductive t : Set := T : t -> t.

 Using Type instead of Set still activates Coq's minimal sort detection...
 Instead, you could also use one specific TypeX obtained via
 Definition TypeX := Type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16203 85f007b7-540e-0410-9357-904b9bb8a0f7
Revised the Ltac trace mechanism so that trace breaking due to
interleaving of ltac and ml code is not visible (this particularly
applies to ltac notation ring, which calls ml-level ring_lookup and
Ring again at the ltac level, resulting in non-localisation of "ring"
errors).

Added also missing LtacLocated checks in Class_instance and Proofview.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
Added propagation of evars unification failure reasons for better
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
Locating errors from consider_remaining_unif_problems if possible
(useful when consider_remaining_unif_problems not called via
pretyping.ml, as e.g. from command.ml).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16206 85f007b7-540e-0410-9357-904b9bb8a0f7
A more informative message when the elimination predicate for
destruct, rewrite, etc. is not well-typed.

Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
Displaying environment and unfolding aliases in "cannot_unify"
error. Maybe displaying environment is making output overly verbose,
but this can also be considered an IDE issue, which would e.g. provide
a button to hide/display environment of the error message...

Also added some "make_all_name_different" which should probably
prevent some anomalies "index to an anonymous variable" at error
reporting time.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16208 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction: same as commit 16203, hopefully without NotASort exns

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16209 85f007b7-540e-0410-9357-904b9bb8a0f7
Minor code cleanups, especially take advantage of Dir_path.is_empty

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7