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

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

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index aa546d773ca7821f43aada14e2562831ce9e66fa..0e9ff4831c4f2469818a4a722b696800174a7154 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -22,6 +22,8 @@ let mk_type n =
      [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+
 (* porcatissima *)
 type reference = Ref of NUri.uri * NReference.spec
 let reference_of_ouri u indinfo =
@@ -621,7 +623,7 @@ let convert_term uri t =
         let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
-    | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
+    | Cic.Sort Cic.CProp -> NCic.Sort (NCic.Type cprop),[]
     | Cic.Sort (Cic.Type u) -> 
           NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[] 
     | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[]