X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=706131f8bc73eb64db0d89f02b31a4d6b760234f;hb=926bd86002f91d2bf2a3ce7376309f5106268959;hp=f34b35748885d8ae4e2ddea34b2c3c8791909dbd;hpb=66be8fbe19e2ccfa0e6a7abeba605152d1322595;p=helm.git

diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml
index f34b35748..706131f8b 100644
--- a/matita/components/ng_paramodulation/nCicProof.ml
+++ b/matita/components/ng_paramodulation/nCicProof.ml
@@ -72,13 +72,13 @@ let debug c _ = c;;
           match t with
           | Terms.Leaf _ 
           | Terms.Var _ -> 
-              let module NCicBlob = NCicBlob.NCicBlob(
+              (*let module NCicBlob = NCicBlob.NCicBlob(
                         struct
                           let metasenv = [] let subst = [] let context = []
                         end)
                           in
-              let module Pp = Pp.Pp(NCicBlob) in  
-               (* prerr_endline ("term: " ^ Pp.pp_foterm ft); 
+               let module Pp = Pp.Pp(NCicBlob) in  
+                  prerr_endline ("term: " ^ Pp.pp_foterm ft); 
                   prerr_endline ("path: " ^ String.concat "," 
                  (List.map string_of_int p1));
                prerr_endline ("leading to: " ^ Pp.pp_foterm t); *)
@@ -192,14 +192,13 @@ let debug c _ = c;;
     ;;
 
   let mk_proof status ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps=
-    let module NCicBlob = 
+    (*let module NCicBlob = 
        NCicBlob.NCicBlob(
 	 struct
 	   let metasenv = [] let subst = [] let context = []
 	 end)
      in
-     let  module Pp = Pp.Pp(NCicBlob) 
-     in
+     let  module Pp = Pp.Pp(NCicBlob) in*)
     let module Subst = FoSubst in
     (*let compose subst1 subst2 =
       let s1 = List.map (fun (x,t) -> (x, Subst.apply_subst subst2 t)) subst1 in
@@ -233,7 +232,7 @@ let debug c _ = c;;
       let lit =match lit with 
           | Terms.Predicate t -> t (* assert false *) 
           | Terms.Equation (l,r,ty,_) -> 
-              Terms.Node [ Terms.Leaf eqP(); ty; l; r]
+              Terms.Node [ Terms.Leaf (eqP()); ty; l; r]
       in
         lit, vl, proof
     in