X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=1487881c1cd0dd92bbca0c23439a1bc4f18d1b66;hb=7b112b0cd39c5ab0db5c28636c0a7f7e36b4d6e2;hp=7bfb6c39c6be23cc73352f8d8d29ba908761e6be;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 7bfb6c39c..1487881c1 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -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 =