auto was compiraing lazy proof terms with = ... fixed

[helm.git] / helm / software / components / tactics / auto.ml

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 3c8c89468e0f46d9334eb95e4819ca32ff2c2ebe..fc9b146f78bc5995d9c64c260dc96d3bff05ee08 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1028,6 +1028,15 @@ let list_union l1 l2 =
   (* TODO ottimizzare compare *)
   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 ;;
+let rec eq_todo l1 l2 =
+  match l1,l2 with
+  | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
+  | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
+    when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
+      if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
+  | [],[] -> true
+  | _ -> false
+;;
 let eat_head todo id fl orlist = 
   let rec aux acc = function
   | [] -> [], acc
@@ -1037,7 +1046,7 @@ let eat_head todo id fl orlist =
         | None -> orlist, acc
         | Some (((gno,_,_),_,_,_), todo11) ->
             (* TODO confronto tra todo da ottimizzare *)
-            if gno = id && todo11 = todo then 
+            if gno = id && eq_todo todo11 todo then 
               aux (list_union fl1 acc) tl
             else 
               aux1 todo11