X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=c4aaa1ca485979031e2b7ad434e8c5783eb4d3f6;hb=d72ed76ff623127f76d91aaff98bd2c109bfcd75;hp=6c0b24327d6fca5dcedc1a0417d8f6caa8999056;hpb=2b4dcaef8f1bef33eeb27e760a1fe518a58edc8a;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 6c0b24327..c4aaa1ca4 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -264,6 +264,12 @@ let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
   eq
 ;;
 
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+  let id = -1 in
+  uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+;;
+
+
 let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
   (weight,proof,(ty,l,r,o),m,id)
 
@@ -706,7 +712,7 @@ let wfo goalproof =
   let rec aux acc id =
     let p,_,_ = proof_of_id id in
     match p with
-    | Exact _ -> id :: acc
+    | Exact _ -> if (List.mem id acc) then acc else id :: acc
     | Step (_,(_,id1, (_,id2), _)) -> 
         let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
         let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
@@ -723,14 +729,18 @@ let string_of_id names id =
         Printf.sprintf "%d = %s: %s = %s" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
     | Step (_,(step,id1, (_,id2), _) ) ->
-        Printf.sprintf "%5d: %s %4d %4d   %s = %s" id
+        Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
           (if step = SuperpositionRight then "SupR" else "Demo") 
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
   with
       Not_found -> assert false
 
 let pp_proof names goalproof =
-  String.concat "\n" (List.map (string_of_id names) (wfo goalproof))
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ 
+  "\ngoal is demodulated with " ^ 
+    (String.concat " " 
+      ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+;;
 
 let build_goal_proof l initial =
   let proof =