Inverters/Inversion:

[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 225269b70fe101eaccf2ed9373c4c1a1634a0e92..1487881c1cd0dd92bbca0c23439a1bc4f18d1b66 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -16,14 +16,14 @@ module Ref = NReference
 let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
 
 let mk_type n = 
- [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+ [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 let is_proof_irrelevant context ty =
@@ -546,7 +546,7 @@ and height_of_term ?(h=ref 0) t =
         in
         let obj = 
           nuri_of_ouri buri,0,[],[],
-            NCic.Fixpoint (false, fl, (`Generated, `Definition)) 
+            NCic.Fixpoint (false, fl, (`Generated, `Definition, `Regular))
         in
         let r = reference_of_ouri buri (Ref.CoFix cofixno) in
         let obj,r =
@@ -607,7 +607,7 @@ and height_of_term ?(h=ref 0) t =
         in
         let obj = 
           nuri_of_ouri buri,height,[],[],
-            NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
+            NCic.Fixpoint (true, fl, (`Generated, `Definition, `Regular)) in
 (*prerr_endline ("H(" ^ UriManager.string_of_uri buri ^ ") = " ^ string_of_int * height);*)
         let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,height)) in
         let obj,r =