diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-17 14:56:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-17 14:56:14 +0000 |
| commit | 98ffcfb509b2438410cb044507efb65ea09ee3be (patch) | |
| tree | 00018501215b060786f529c01a254081e6391067 /pretyping/pretype_errors.ml | |
| parent | f5e644a53c69392f94eae01dd71ab79b4700a892 (diff) | |
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
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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) = |