From eb254f3de9c9eaad08b084231cf78d64bf585012 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 May 2008 11:41:21 +0000 Subject: [PATCH] renamed add_le_constraint to add_constraint since it adds both le and lt constraints --- helm/software/components/ng_kernel/nCicEnvironment.ml | 4 ++-- helm/software/components/ng_kernel/nCicEnvironment.mli | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index fa229d6f6..de785bde8 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -38,9 +38,9 @@ let universe_leq a b = raise (BadConstraint (lazy "trying to check if a universe is less or equal than an inferred universe")) -let universe_eq a b = universe_leq b a || universe_leq a b +let universe_eq a b = universe_leq b a && universe_leq a b -let add_le_constraint strict a b = +let add_constraint strict a b = match a,b with | [false,a2],[false,b2] -> if not (le_path_uri [] strict a2 b2) then ( diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 7fa352901..272530a1a 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -24,11 +24,11 @@ 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 +(* add_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 add_constraint: bool -> NCic.universe -> NCic.universe -> unit val get_checked_def: NReference.reference -> -- 2.39.2