Bug fixed in computation of heights: a constant must have height greater than its...

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0e6ebe32f5fd98cccfecaca35fae62fa844a7d36..49b0e676b7b46b0c3a2cadfe14dad7fd572a95fe 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -437,8 +437,8 @@ and height_of_term ?(h=ref 0) t =
  | Cic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
  | Cic.Appl l -> List.iter aux l
  | Cic.MutCase (_,_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
- | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) ->  aux ty; aux bo) fl
- | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) ->  aux ty; aux bo) fl
+ | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) ->  aux ty; aux bo) fl; incr h
+ | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) ->  aux ty; aux bo) fl; incr h
  in
    aux t;
    1 + !h
@@ -511,7 +511,7 @@ let convert_term uri t =
           UriManager.uri_of_string 
            (UriManager.buri_of_uri uri^"/"^
             UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con") in
-        let height = height_of_term fix in
+        let height = height_of_term fix - 1 in
         let bad_bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
             (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) ->