use named types to force some constraints asap

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c4940e08989c259b403aff5e24d74034509ec93a..c324b0ec6d90b0360eb75ebebf6d7af4c9ed19fe 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -435,6 +435,9 @@ and unify test_eq_only metasenv subst context t1 t2 =
              with Invalid_argument _ -> 
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+       | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
+                NCicUntrusted.metas_of_term subst context t2 = [] -> 
+                  raise (fail_exc metasenv subst context t1 t2)
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
      (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in
@@ -486,20 +489,22 @@ and unify test_eq_only metasenv subst context t1 t2 =
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
-          let rec check_stack l1 l2 r (metasenv, subst) =
+          let rec check_stack l1 l2 r todo =
             match l1,l2,r with
-            | x1::tl1, x2::tl2, r::tr ->
-                check_stack tl1 tl2 tr 
-                  (unif_from_stack x1 x2 r metasenv subst)
-            | x1::tl1, x2::tl2, [] ->
-                check_stack tl1 tl2 [] 
-                  (unif_from_stack x1 x2 true metasenv subst)
+            | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
+            | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
             | l1, l2, _ -> 
-                fo_unif test_eq_only metasenv subst
-                   (NCicReduction.unwind (k1,e1,t1,List.rev l1)) 
-                   (NCicReduction.unwind (k2,e2,t2,List.rev l2))
+               NCicReduction.unwind (k1,e1,t1,List.rev l1),
+                NCicReduction.unwind (k2,e2,t2,List.rev l2),
+                todo
           in
-        try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
+        let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
+        try
+         let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
+         List.fold_left
+          (fun (metasenv,subst) (x1,x2,r) ->
+            unif_from_stack x1 x2 r metasenv subst
+          ) (metasenv,subst) todo
         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
            unif_machines metasenv subst (small_delta_step m1 m2)
       (*D*)  in outside(); rc with exn -> outside (); raise exn