some debug prints/stats

[helm.git] / helm / ocaml / tactics / paramodulation / utils.ml

diff --git a/helm/ocaml/tactics/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml
index 3cafedd54bddd94f18d163fac0976c7d9a75572a..b2555cdb4b1f9323262a5e164615d942818d300b 100644 (file)
--- 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
 (*