saturate cust be called with delta=0

[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 f13f35fbfb9c6552a621aada1db5aee60e40b1a9..1c74ac9e5b259d74fef23108a89aee864f88fb41 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -19,7 +19,7 @@ let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
        NCic.Const ref
   | EqInd_l -> 
@@ -31,7 +31,7 @@ let default_sig = function
       let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
        NCic.Const ref
   | Refl ->
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
        NCic.Const ref
 
@@ -68,7 +68,7 @@ let set_reference_of_oxuri reference_of_oxuri =
 (* let debug c r = prerr_endline r; c *)
 let debug c _ = c;;
 
-  let eqP() = debug (!eqsig Eq) "eqp"  ;;
+  let eqP() = debug (!eqsig Eq) "eq"  ;;
   let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
   let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";; 
   let eq_refl() = debug (!eqsig Refl) "refl";;