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

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 793da99404c568c5b6cf48e57ffe2effb938ed67..660edb2f59b7408e9cc7acdc1fedca119c02be07 100644 (file)
--- a/helm/software/components/binaries/transcript/.depend
+++ b/helm/software/components/binaries/transcript/.depend
@@ -6,7 +6,9 @@ v8Lexer.cmo: v8Parser.cmi options.cmo
 v8Lexer.cmx: v8Parser.cmx options.cmx 
 grafite.cmo: types.cmo options.cmo grafite.cmi 
 grafite.cmx: types.cmx options.cmx grafite.cmi 
-engine.cmo: v8Parser.cmi v8Lexer.cmo types.cmo grafite.cmi engine.cmi 
-engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi 
+engine.cmo: v8Parser.cmi v8Lexer.cmo types.cmo options.cmo grafite.cmi \
+    engine.cmi 
+engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx options.cmx grafite.cmx \
+    engine.cmi 
 top.cmo: options.cmo engine.cmi 
 top.cmx: options.cmx engine.cmx 

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