From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 11 Dec 2008 22:39:49 +0000 (+0000)
Subject: Applications are now processed from left to right.
X-Git-Tag: make_still_working~4419
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99a4ad6d8760a75b7f4464d570cec0e85efe2bb8;p=helm.git

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 90a5d3ce6..c324b0ec6 100644
--- 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