Big change:

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

diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml
index c5290694bfd96a4c5179b70eaeb665d8a742d3d7..f9b60ba26d916ca14383192c0633789bdd855bc3 100644 (file)
--- a/matita/components/ng_paramodulation/nCicProof.ml
+++ b/matita/components/ng_paramodulation/nCicProof.ml
@@ -19,19 +19,19 @@ let get_sig = fun x -> !eqsig x;;
 
 let default_sig = function
   | Eq -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
         NCic.Const ref
   | EqInd_l -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/rewrite_l.con" in
       let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
         NCic.Const ref
   | EqInd_r -> 
-      let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/rewrite_r.con" in
       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/eq.ind" in
+      let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in
       let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
         NCic.Const ref
 
@@ -39,32 +39,6 @@ let set_default_sig () =
   (*prerr_endline "setting default sig";*)
   eqsig := default_sig
 
-let set_reference_of_oxuri reference_of_oxuri = 
-  prerr_endline "setting oxuri in nCicProof";
-  let nsig = function
-    | Eq -> 
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))  
-    | EqInd_l -> 
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq_ind.con"))
-    | EqInd_r -> 
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq_elim_r.con"))
-    | Refl ->
-        NCic.Const
-          (reference_of_oxuri 
-             (UriManager.uri_of_string 
-                "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
-  in eqsig:= nsig
-  ;;
-
 (* let debug c r = prerr_endline r; c *)
 let debug c _ = c;;