Applications are now processed from left to right.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 90a5d3ce63d7e81c94028136e0ed188e1a5c0bc8..c324b0ec6d90b0360eb75ebebf6d7af4c9ed19fe 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -489,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