From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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