X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.mli;h=58f97a3f22dea41c5b32cbc8bdd5ccec0199fa9f;hb=7d9753115cb26bf27a739e9e1d753fd60b185c17;hp=5fafaf54f386510e0f5032e4f0170be1a1e0b502;hpb=3c1a432c1612f8ed21f5b2220005599c4d9da1d5;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicBlob.mli b/helm/software/components/ng_paramodulation/nCicBlob.mli index 5fafaf54f..58f97a3f2 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.mli +++ b/helm/software/components/ng_paramodulation/nCicBlob.mli @@ -11,6 +11,8 @@ (* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *) +val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit + module type NCicContext = sig val metasenv : NCic.metasenv @@ -18,5 +20,6 @@ module type NCicContext = val context : NCic.context end -module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term +module NCicBlob(C : NCicContext) : Terms.Blob +with type t = NCic.term and type input = NCic.term