From e2183a68ca472d7605be0447a9c7cc9eab27f509 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:27:05 +0000
Subject: Proper typing of metavariables, type errors were completely ignored
 before... Use sort constraint checking as in evarconv as well

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13990 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7b01134e00..d2ee780c6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -256,6 +256,16 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
 	| Evar ev, _ -> sigma,metasubst,((curenv, ev,cN)::evarsubst)
 	| _, Evar ev -> sigma,metasubst,((curenv, ev,cM)::evarsubst)
+
+	| Sort s1, Sort s2 ->
+	    (try 
+	       let sigma' = 
+		 if cv_pb = Cumul 
+		 then Evd.set_leq_sort sigma s1 s2 
+		 else Evd.set_eq_sort sigma s1 s2 
+	       in (sigma', metasubst, evarsubst)
+	     with _ -> error_cannot_unify_local curenv sigma (m,n,cM))
+	      
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
 	    unirec_rec (push (na,t1) curenvnb) topconv true
 	      (unirec_rec curenvnb topconv true substn t1 t2) c1 c2
@@ -612,23 +622,18 @@ let unify_to_type env sigma flags c status u =
   let t = get_type_of env sigma c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
   let u = Tacred.hnf_constr env sigma u in
-    try
-      if status = IsSuperType then
+    if status = IsSuperType then
+      unify_0 env sigma Cumul flags u t
+    else if status = IsSubType then
+      unify_0 env sigma Cumul flags t u
+    else
+      try unify_0 env sigma Cumul flags t u
+      with e when precatchable_exception e ->
 	unify_0 env sigma Cumul flags u t
-      else if status = IsSubType then
-	unify_0 env sigma Cumul flags t u
-      else
-	try unify_0 env sigma Cumul flags t u
-	with e when precatchable_exception e ->
-	  unify_0 env sigma Cumul flags u t
-    with e when precatchable_exception e ->
-      (sigma,[],[])
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
-  if occur_meta_or_existential mvty or is_arity env sigma mvty then
     unify_to_type env sigma flags c status mvty
-  else (sigma,[],[])
 
 (* Move metas that may need coercion at the end of the list of instances *)
 
-- 
cgit v1.2.3