X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=c5290694bfd96a4c5179b70eaeb665d8a742d3d7;hb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;hp=df6f949b603c867128b5d31634cf72091199ab9e;hpb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index df6f949b6..c5290694b 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -218,7 +218,6 @@ let debug c _ = c;;
     in aux ft (List.rev pl)
     ;;
 
-  (* we should better split forward and backward rewriting *)
   let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
     let module NCicBlob = 
        NCicBlob.NCicBlob(
@@ -254,7 +253,7 @@ let debug c _ = c;;
     let get_literal id =
       let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
       let lit =match lit with 
-          | Terms.Predicate t -> assert false 
+          | Terms.Predicate t -> t (* assert false *) 
           | Terms.Equation (l,r,ty,_) -> 
               Terms.Node [ Terms.Leaf eqP(); ty; l; r]
       in