the tactic now returns as open goals the open metas in the proof

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

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 547a235590a7991ddc8144f94f0ade20984b7aa7..a3894fd84cdbfa374ecc3e570ac8bbbb2fad57df 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -541,11 +541,11 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
           subst, menv
         with CicUtil.Meta_not_found m ->
           let names = names_of_context context in
-          debug_print
-            (lazy
+          (*debug_print
+            (lazy*) prerr_endline 
                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
                   (CicPp.pp t1 names) (CicPp.pp t2 names)
-                  (print_metasenv menv) (print_metasenv metasenv)));
+                  (print_metasenv menv) (print_metasenv metasenv));
           assert false
       )
     | _, C.Meta _ -> unif subst menv t s