more cleanup

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 5cc6e811e293fe5e80afd926a1ab32e5e1e7254c..fac0197df0ca1add3502bc0c599da4305727db0a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -111,7 +111,8 @@ module OrderedEquality = struct
         match Pervasives.compare w1 w2 with
         | 0 -> 
             let res = (List.length m1) - (List.length m2) in 
-            if res <> 0 then res else Pervasives.compare eq1 eq2
+            if res <> 0 then res else 
+              Pervasives.compare eq1 eq2
         | res -> res 
 end 
 
@@ -1396,47 +1397,6 @@ let reset_refs () =
   Equality.reset ();
 ;;
 
-let interactive_comparison context t1 t2 =
-  let rc = ref [] in
-  let module P = Printf in
-  let rec aux n context t1 t2 =
-(*    let names = names_of_context context in*)
-    let pp t1 t2 = () (*
-      P.eprintf "%s%s === %s\n" (String.make n ' ') 
-      (CicPp.pp t1 names) (CicPp.pp t2 names) *)
-    in
-    match t1,t2 with
-    | _, Cic.Appl [Cic.Const(uri,_);t2] when 
-      UriManager.eq uri (UriManager.uri_of_string
-      "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2
-    | Cic.Implicit _, _ -> pp t1 t2
-    | Cic.Meta (n,_), _ -> 
-        rc := (n,t2,context) :: !rc;
-        pp (Cic.Meta(n,[])) t2
-    | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2
-    | Cic.Appl l1,Cic.Appl l2 -> 
-        if List.length l1 <> List.length l2 then
-          begin
-            prerr_endline "ERROR: application with diff num of args";
-            pp t1 t2
-          end
-        else
-          List.iter2 (aux (n+1) context) l1 l2
-    | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) ->
-        let context = (Some (name,(Cic.Decl s)))::context in
-        aux (n+1) context t1 t2
-    | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 -> 
-        pp t1 t2
-    | _,_ -> pp t1 t2
-  in
-  aux 0 context t1 t2;
-  List.iter (fun (n,t,ctx) -> 
-    let names = names_of_context ctx in 
-    Printf.eprintf "%d := %s\n" n (CicPp.pp t  names)) 
-    (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc))
-;;
-
-
 let saturate 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
@@ -1640,7 +1600,6 @@ let saturate
             | CicRefine.AssertFailure s -> 
                 prerr_endline "FAILURE IN REFINE";
                 prerr_endline (Lazy.force s);
-                interactive_comparison context cic_proof_new cic_proof;
                 assert false
           in
           if List.length newmetasenv_new <> 0 then