X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.mli;h=7fa352901fd63ea2b949d6d80a8a5262b315dd19;hb=15bc0d34ae5f72cb31ec383e1ac48ad53f06a725;hp=048dd7b96a46bd8cde85da950bbe556b075214b4;hpb=cf4da27b865107f9b89f3d2726f14d6e2694c548;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 048dd7b96..7fa352901 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -14,11 +14,22 @@ exception CircularDependency of string Lazy.t;; exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t;; +exception BadConstraint of string Lazy.t;; val get_checked_obj: NUri.uri -> NCic.obj val get_relevance: NReference.reference -> bool list +val type0: NCic.universe +(* universe_* raise BadConstraints if the second arg. is an inferred universe *) +val universe_eq: NCic.universe -> NCic.universe -> bool +val universe_leq: NCic.universe -> NCic.universe -> bool +(* add_le_constraint raise BadConstraint in case of universe inconsistency + or if the second argument is an inferred universe + true -> strict check (<); false -> loose check (<=) +*) +val add_le_constraint: bool -> NCic.universe -> NCic.universe -> unit + val get_checked_def: NReference.reference -> NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int