From: Enrico Tassi Date: Thu, 15 May 2008 15:08:57 +0000 (+0000) Subject: Bug fixed in computation of heights: a constant must have height greater than its... X-Git-Tag: make_still_working~5198 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8ede07ed1f9b4937fc333f3438f635a0530e3a76;p=helm.git Bug fixed in computation of heights: a constant must have height greater than its constant__s --- diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 0e6ebe32f..49b0e676b 100644 --- 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) ->