All the debug_print are now lazy.

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 698175d1b13b1f5545ff369a469092c056816334..5b84bb72ade6e5afc5b1b76354b3bef66fa28a3d 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -182,9 +182,9 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
 (*         if not (fst (CicReduction.are_convertible *)
 (*                        ~metasenv context termty ty ugraph)) then ( *)
-(* (\*           debug_print ( *\) *)
+(* (\*           debug_print (lazy ( *\) *)
 (* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
-(* (\*               (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
+(* (\*               (CicPp.pp termty names) (CicPp.pp ty names))); *\) *)
 (*           find_matches metasenv context ugraph lift_amount term termty tl *)
 (*         ) else *)
           let do_match c other eq_URI =
@@ -253,9 +253,9 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
 (*         if not (fst (CicReduction.are_convertible *)
 (*                        ~metasenv context termty ty ugraph)) then ( *)
-(* (\*           debug_print ( *\) *)
+(* (\*           debug_print (lazy ( *\) *)
 (* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
-(* (\*               (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
+(* (\*               (CicPp.pp termty names) (CicPp.pp ty names))); *\) *)
 (*           find_all_matches ~unif_fun metasenv context ugraph *)
 (*             lift_amount term termty tl *)
 (*         ) else *)