From: Claudio Sacerdoti Coen Date: Mon, 15 Feb 2010 12:41:44 +0000 (+0000) Subject: The height of fixpoint applications was not computed correctly. X-Git-Tag: make_still_working~3043 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=47805b28c04bff91a6dd743bf30c6e412e1b4583;p=helm.git The height of fixpoint applications was not computed correctly. --- diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index e6010808b..e45873bc8 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -13,10 +13,14 @@ open Printf let debug = ref false let debug_print ?(depth=0) s = +() (* if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () +*) (* let print = debug_print *) -let print ?(depth=0) s = +let print ?(depth=0) s = () +(* prerr_endline (String.make depth '\t'^Lazy.force s) +*) let debug_do f = if !debug then f () else () @@ -1300,8 +1304,8 @@ let keys_of_term status t = let keys = let _, ty = term_of_cic_term status ty (ctx_of ty) in match ty with - | NCic.Const (NReference.Ref (_,NReference.Def h)) - | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_) + | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h)))) + | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_) when h > 0 -> let _,ty,_= saturate status ~delta:(h-1) orig_ty in ty::keys @@ -1323,8 +1327,8 @@ let mk_th_cache status gl = List.fold_left (fun (status, i, idx) _ -> let t = mk_cic_term ctx (NCic.Rel i) in - debug_print(lazy("indexing: "^ppterm status t)); let status, keys = keys_of_term status t in + debug_print(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys))); let idx = List.fold_left (fun idx k -> InvRelDiscriminationTree.index idx k t) idx keys