CProp dropped in favour of a cprop universe exported from NCicEnvironment,

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index bd0587a43a53f3fd6afb5f8dda9954167c9716f1..46552d5aa690e649354315ead787b6014da77716 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -19,7 +19,8 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t;;
 exception BadConstraint of string Lazy.t;;
 
-let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+let type0 = []
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
 
 let le_constraints = ref [] (* strict,a,b *)