]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_paramodulation/nCicBlob.ml
fix queries
[helm.git] / matita / components / ng_paramodulation / nCicBlob.ml
index fb9ee62457b2c2e20257ac08368ac4f09fffa6f1..d9679bf3abdd5c36de60622e7f28a367cd9b5328 100644 (file)
@@ -33,18 +33,6 @@ let setoid_eq =
 
 let set_default_eqP() = eqPref := default_eqP
 
-let set_reference_of_oxuri f = 
-  let eqnew = function 
-      _ -> 
-       let r = f(UriManager.uri_of_string 
-          "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
-       in
-         NCic.Const r
-  in
-    eqPref := eqnew
-;;
-
-
 module type NCicContext =
   sig
     val metasenv : NCic.metasenv