X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Futils.ml;h=b2555cdb4b1f9323262a5e164615d942818d300b;hb=b555e6b8c27c765a4611dda9528963ebff116412;hp=3cafedd54bddd94f18d163fac0976c7d9a75572a;hpb=b1527286e32c8651d65619af61e3f638b3b89f8d;p=helm.git

diff --git a/helm/ocaml/tactics/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml
index 3cafedd54..b2555cdb4 100644
--- a/helm/ocaml/tactics/paramodulation/utils.ml
+++ b/helm/ocaml/tactics/paramodulation/utils.ml
@@ -131,7 +131,7 @@ let sig_order t1 t2 =
     else 
       begin
 	prerr_endline ("t1 = "^(CicPp.ppterm t1));
-	prerr_endline ("t2 = "^(CicPp.ppterm t2)); flush;
+	prerr_endline ("t2 = "^(CicPp.ppterm t2)); 
 	assert false
       end
   with 
@@ -635,9 +635,9 @@ let rec lpo t1 t2 =
 
 
 (* settable by the user... *)
-(* let compare_terms = ref nonrec_kbo;; *)
+let compare_terms = ref nonrec_kbo;; 
 (* let compare_terms = ref ao;; *)
-let compare_terms = ref rpo;;
+(* let compare_terms = ref rpo;; *)
 
 let guarded_simpl context t = t
 (*