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
---
 pretyping/pretype_errors.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f5870a8c0b..5403c1e99e 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) =
-- 
cgit v1.2.3