From 16ea6252339bed9901fff48b5883f4d471a88e7a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Apr 2009 10:13:28 +0000
Subject: Backtrack on 12061 (type checking for bug #2084 too strong as soon as
 we use Type instead of sort variables for unknown levels in unification).

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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0b3eedcb83..217376acc4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -495,7 +495,8 @@ let unify_to_type env evd flags c u =
   let t = get_type_of env sigma c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
-  unify_0 env sigma Cumul flags t u
+  try unify_0 env sigma Cumul flags t u
+  with e when precatchable_exception e -> ([],[])
 
 let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
-- 
cgit v1.2.3