From 9a431a1b43dead6d692c942986a25f0f8986465a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 28 Feb 2013 07:33:41 +0000
Subject: Repairing r16205: errors raised by check_evar_instance were no longer
 trapped by solve_simple_eqn.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretype_errors.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 91d24ec698..72cc6502a2 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -22,7 +22,7 @@ type unification_error =
   | NoCanonicalStructure
   | ConversionFailed of env * constr * constr
   | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key
+  | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency
 
 type pretype_error =
-- 
cgit v1.2.3