X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=5f8ed1733ccfd44888287e0affc9a6b380a923a1;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=cabca8259aefc524e89ed5b0e8e74f27049df70e;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_paramodulation/nCicProof.ml b/matitaB/components/ng_paramodulation/nCicProof.ml
index cabca8259..5f8ed1733 100644
--- 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
@@ -238,24 +231,7 @@ let debug c _ = c;;
       let lit = Subst.apply_subst subst lit in
         extract status 0 [] lit in
     (* composition of all subst acting on goal *)
-    let res_subst =
-      let rec rsaux ongoal acc = 
-	function
-	  | [] -> acc (* is the final subst for refl *)
-	  | id::tl when ongoal ->
-            let lit,vl,proof = get_literal id in
-	      (match proof with
-		| Terms.Exact _ -> rsaux ongoal acc tl
-		| Terms.Step (_, _, _, _, _, s) ->
-		    rsaux ongoal (s@acc) tl)
-	  | id::tl -> 
-	    (* subst is the the substitution for refl *)
-	    rsaux (id=mp) subst tl
-      in 
-      let r = rsaux false [] steps in
-	(* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
-           prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
-      r
+    let res_subst = subst 
     in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1