The Blob is not abstracted on the context any more.

[helm.git] / matitaB / components / ng_paramodulation / nCicProof.ml

diff --git a/matitaB/components/ng_paramodulation/nCicProof.ml b/matitaB/components/ng_paramodulation/nCicProof.ml
index cabca8259aefc524e89ed5b0e8e74f27049df70e..50c25315f91bd7ab1758892c857d6d7c6b854fde 100644 (file)
--- a/matitaB/components/ng_paramodulation/nCicProof.ml
+++ b/matitaB/components/ng_paramodulation/nCicProof.ml
@@ -73,11 +73,7 @@ let debug c _ = c;;
           match t with
           | Terms.Leaf _ 
           | Terms.Var _ -> 
-              let module NCicBlob = NCicBlob.NCicBlob(
-                        struct
-                          let metasenv = [] let subst = [] let context = []
-                        end)
-                          in
+              let module NCicBlob = NCicBlob.NCicBlob in
               let module Pp = Pp.Pp(NCicBlob) in  
                prerr_endline ("term: " ^ Pp.pp_foterm ft);
                prerr_endline ("path: " ^ String.concat "," 
@@ -194,10 +190,7 @@ let debug c _ = c;;
 
   let mk_proof status ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps=
     let module NCicBlob = 
-       NCicBlob.NCicBlob(
-        struct
-          let metasenv = [] let subst = [] let context = []
-        end)
+       NCicBlob.NCicBlob
      in
      let  module Pp = Pp.Pp(NCicBlob) 
      in