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 e6010808be96e90216eb511e0b4df0c256bff585..e45873bc8e927435f506dd65ae8fc0706b0716dd 100644 (file)
--- 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