modification de clenv_merge:

on ajoute en premier lieu les contraintes concernant le terme puis apres
celles concernant le type de chaque instantiation, au lieu d'alterner l'ajout
de contraintes de terme et de type. A l'essai.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2682 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 12 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ec79b91f61..ce56a980d5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -560,7 +560,9 @@ let clenv_instance_type_of ce c =
    or in evars, possibly generating new unification problems; if [b]
    is true, unification of types of metas is required *)
 
-let clenv_merge with_types =
+let clenv_merge with_types metas evars clenv =
+  let ty_metas = ref [] in
+  let ty_evars = ref [] in
   let rec clenv_resrec metas evars clenv =
     match (evars,metas) with
       | ([], []) -> clenv
@@ -603,18 +605,25 @@ let clenv_merge with_types =
               unify_0 CONV clenv.hook (clenv_value clenv mv).rebus n in
             clenv_resrec (metas'@t) evars' clenv
     	  else
-	    let mc,ec =
-	      let mvty = clenv_instance_type clenv mv in
+            begin
 	      if with_types (* or occur_meta mvty *) then
-		(try 
-		let nty = clenv_type_of clenv 
-			    (clenv_instance clenv (mk_freelisted n)) in
-		unify_0 CUMUL clenv.hook nty mvty
-		with e when Logic.catchable_exception e -> ([],[]))
-	      else ([],[]) in
-	    clenv_resrec (mc@t) ec (clenv_assign mv n clenv)
-
-  in clenv_resrec
+	        (let mvty = clenv_instance_type clenv mv in
+		try 
+		  let nty = clenv_type_of clenv 
+			      (clenv_instance clenv (mk_freelisted n)) in
+		  let (mc,ec) = unify_0 CUMUL clenv.hook nty mvty in
+                  ty_metas := mc @ !ty_metas;
+                  ty_evars := ec @ !ty_evars
+		with e when Logic.catchable_exception e -> ());
+	      clenv_resrec t [] (clenv_assign mv n clenv)
+            end in
+  (* merge constraints *)
+  let clenv' = clenv_resrec metas evars clenv in
+  if with_types then
+    (* merge constraints about types: if they fail, don't worry *)
+    try clenv_resrec !ty_metas !ty_evars clenv'
+    with e when Logic.catchable_exception e -> clenv'
+  else clenv'
 
 (* [clenv_unify M N clenv]
    performs a unification of M and N, generating a bunch of