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

3 files changed, 7 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index a8de06318..065892e5a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,7 @@ Specification Language
 - The syntax "x -> y" is now declared at level 99. In particular, it has
   now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
   (possible source of incompatibilities)
+- Slight changes in unification error messages.
 
 Tactics
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f5870a8c0..5403c1e99 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -154,6 +154,7 @@ let error_cannot_unify_loc loc env sigma ?reason (m,n) =
   Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason)))
 
 let error_cannot_unify env sigma ?reason (m,n) =
+  let env, m, n = contract2 env m n in
   raise (PretypeError (env, sigma,CannotUnify (m,n,reason)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 14202a32a..18638ad8b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -189,6 +189,7 @@ let explain_unification_error env sigma p1 p2 = function
         spc () ++ str "(Universe inconsistency)"
 
 let explain_actual_type env sigma j t reason =
+  let env = make_all_name_different env in
   let j = Evarutil.j_nf_betaiotaevar sigma j in
   let t = Reductionops.nf_betaiota sigma t in
   let pe = pr_ne_context_of (str "In environment") env in
@@ -456,19 +457,21 @@ let explain_wrong_case_info env ind ci =
     spc () ++ pc ++ str "."
 
 let explain_cannot_unify env sigma m n e =
+  let env = make_all_name_different env in
   let m = Evarutil.nf_evar sigma m in
   let n = Evarutil.nf_evar sigma n in
   let pm = pr_lconstr_env env m in
   let pn = pr_lconstr_env env n in
   let ppreason = explain_unification_error env sigma m n e in
-  str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
+  let pe = pr_ne_context_of (str "In environment") (mt ()) env in
+  pe ++ str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++
   str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "."
 
 let explain_cannot_unify_local env sigma m n subn =
   let pm = pr_lconstr_env env m in
   let pn = pr_lconstr_env env n in
   let psubn = pr_lconstr_env env subn in
-    str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
+    str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++
       str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++
       psubn ++ str " contains local variables."