some bugs fixed

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 746a2faead0fcfc567e2d8c6a1dd45231c8be509..09a0234575e2dc918d116500ea80ba4f981b403e 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1141,6 +1141,9 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (term, termty)::tl ->
+        debug_print (
+          Printf.sprintf "Examining: %s (%s)"
+            (CicPp.ppterm term) (CicPp.ppterm termty));
         let res, newmeta = 
           match termty with
           | C.Prod (name, s, t) ->