X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.mli;h=862d7148432f5a6ba7525780d5e0b8d04f36b3f9;hb=421056da7b3e1d6b9d91d72092b4f3c3232a00ce;hp=c4fa396cc1d6d493afb4d80644c3b818e0cc2eda;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index c4fa396cc..862d71484 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -16,6 +16,8 @@ exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; +val set_get_obj: (NUri.uri -> NCic.obj) -> unit + val get_checked_obj: NUri.uri -> NCic.obj val get_relevance: NReference.reference -> bool list @@ -33,8 +35,6 @@ val add_constraint: bool -> NCic.universe -> NCic.universe -> unit val sup : NCic.universe -> NCic.universe option val pp_constraints: unit -> string -val resolve_universe: string -> NUri.uri option - val get_checked_def: NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int