X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.mli;h=a8b6a7b7e045bdef55836df7753e361fa6cad802;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=16a8c33a2b06b64e657f1180cfd084d81298e4a4;hpb=f7bfbdc706a75256c0e9b15ecc242175f562eb71;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicBlob.mli b/helm/software/components/ng_paramodulation/nCicBlob.mli index 16a8c33a2..a8b6a7b7e 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.mli +++ b/helm/software/components/ng_paramodulation/nCicBlob.mli @@ -11,6 +11,10 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) +val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit +val set_eqP: NCic.term -> unit +val set_default_eqP: unit -> unit + module type NCicContext = sig val metasenv : NCic.metasenv