we revisited the implementation of the destruct tactic in the perspective of joining...

[helm.git] / helm / software / components / tactics / paramodulation / utils.ml

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index 00d745fd906fb1ec2ac0aa6fa88a11faa17b7515..c6e64b898753f435e54a959a4d5c09dfc216e1c6 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -753,8 +753,7 @@ let guarded_simpl ?(debug=false) context t =
     if t = t' then t else
       begin
        let simpl_order = !compare_terms t t' in
-       if debug then
-         prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
+        debug_print (lazy ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t')));
        if simpl_order = Gt then (if debug then prerr_endline "GT";t')
        else (if debug then prerr_endline "NO_GT";t)
       end