proof patching!

[helm.git] / helm / software / components / ng_paramodulation / nCicBlob.ml

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 1e5e67979fb2f0f7f8b31010898b4343dcf99f61..46710db2137646dff91b87a887a6e01e542b5881 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -197,7 +197,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
           let amount = List.length seen in
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
-            ((*prerr_endline ("Reached meeting point, id=" ^ (string_of_int id));*)
+            ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
             assert (vl = []);  
              NCic.LetIn ("clause_" ^ string_of_int id, 
                 extract amount vl lit,