From 4ccc7ef7fe3d43fb0f882768d2818a54e24c8857 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 26 Sep 2008 09:27:51 +0000
Subject: [PATCH] auto was compiraing lazy proof terms with = ... fixed

---
 helm/software/components/binaries/transcript/.depend |  6 ++++--
 helm/software/components/tactics/auto.ml             | 11 ++++++++++-
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 793da9940..660edb2f5 100644
--- 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 3c8c89468..fc9b146f7 100644
--- 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
-- 
2.39.2