From 98ffcfb509b2438410cb044507efb65ea09ee3be Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 17 Feb 2013 14:56:14 +0000 Subject: 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 --- CHANGES | 1 + pretyping/pretype_errors.ml | 1 + toplevel/himsg.ml | 7 +++++-- 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." -- cgit v1.2.3