From: Andrea Asperti Date: Wed, 2 Dec 2009 09:43:20 +0000 (+0000) Subject: Generalized initialization of eqP. X-Git-Tag: make_still_working~3191 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc2c1fd44709365c30436fdfe320b324b2592ba6;p=helm.git Generalized initialization of eqP. --- diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 05867b00e..b02a1ebc0 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -11,8 +11,27 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) -let reference_of_oxuri = ref (fun _ -> assert false);; -let set_reference_of_oxuri f = reference_of_oxuri := f;; +let eqPref = ref (fun _ -> assert false);; +let set_eqP t = eqPref := fun _ -> t;; + +let default_eqP() = + let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in + let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in + NCic.Const ref + +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 @@ -80,14 +99,8 @@ with type t = NCic.term and type input = NCic.term = struct let sty = embed sty in proof, sty ;; - - let eqP = - let r = - !reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") - in - NCic.Const r + + let eqP = (!eqPref)() ;; end