update in ground_2

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

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index df6f949b603c867128b5d31634cf72091199ab9e..c5290694bfd96a4c5179b70eaeb665d8a742d3d7 100644 (file)
--- 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