From 22c254f98842cf7b6f94189625e4936a169bdfb1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 May 2008 23:01:48 +0000 Subject: [PATCH] We do not need to give cprop a special status yet. --- helm/software/components/ng_kernel/nCicEnvironment.ml | 1 - helm/software/components/ng_kernel/nCicEnvironment.mli | 1 - 2 files changed, 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 46552d5aa..106d92706 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -20,7 +20,6 @@ exception BadDependency of string Lazy.t;; exception BadConstraint of string Lazy.t;; let type0 = [] -let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")] let le_constraints = ref [] (* strict,a,b *) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index d3c60a3c2..67b3857d1 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -21,7 +21,6 @@ val get_checked_obj: NUri.uri -> NCic.obj val get_relevance: NReference.reference -> bool list val type0: NCic.universe -val cprop: 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 -- 2.39.2