X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=bc6730376640e654753258dd48a5ef252799f8a7;hb=6d31b4fb75d8ae3b898790e56aa9694fed12d040;hp=572cd4e28932d25c1bf1ed119ade0c8a4fd95bb5;hpb=9581b03be2b2bc830820b93992920aaa2c021cc9;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 572cd4e28..bc6730376 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -72,8 +72,12 @@ let print_stat status tbl =
   let vcompare (_,v1) (_,v2) =
     Pervasives.compare (relevance v1) (relevance v2) in
   let l = List.sort vcompare l in
+  let short_name r = 
+    Filename.chop_extension 
+      (Filename.basename (NReference.string_of_reference r))
+  in
   let vstring (a,v)=
-      NotationPp.pp_term status (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
+      short_name a ^ ": rel = " ^
       (string_of_float (relevance v)) ^
       "; uses = " ^ (string_of_int !(v.uses)) ^
       "; nom = " ^ (string_of_int !(v.nominations)) in
@@ -288,10 +292,11 @@ let auto_eq_check eq_cache status =
 ;;
 
 let index_local_equations eq_cache status =
+  noprint (lazy "indexing equations");
   let open_goals = head_goals status#stack in
   let open_goal = List.hd open_goals in
-  debug_print (lazy ("indexing equations for " ^ string_of_int open_goal));
   let ngty = get_goalty status open_goal in
+  let _,_,metasenv,subst,_ = status#obj in
   let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
   let c = ref 0 in
   List.fold_left 
@@ -299,12 +304,12 @@ let index_local_equations eq_cache status =
        c:= !c+1;
        let t = NCic.Rel !c in
          try
-           let ty = NCicTypeChecker.typeof status [] [] ctx t in
+           let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
-             (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
-              NCicParamod.forward_infer_step eq_cache t ty)
+             (noprint(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+              NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
            else 
-             (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
+             (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
               eq_cache)
          with 
            | NCicTypeChecker.TypeCheckerFailure _
@@ -1014,7 +1019,7 @@ let perforate_small status subst metasenv context t =
   let rec aux = function
     | NCic.Appl (hd::tl) ->
 	let map t =
-	  let s = sort_of status subst metasenv context t in
+	    let s = sort_of status subst metasenv context t in
 	    match s with
 	      | NCic.Sort(NCic.Type [`Type,u])
 		  when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
@@ -1060,7 +1065,7 @@ let get_candidates ?(smart=true) depth flags status cache signature gty =
             let raw_weak = 
               perforate_small status subst metasenv context raw_gty in
             let weak = mk_cic_term context raw_weak in
-            debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
+            noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
               Some raw_weak, Some (weak)
 	| _ -> None,None
     else None,None
@@ -1186,7 +1191,6 @@ let applicative_case depth signature status flags gty cache =
 exception Found
 ;;
 
-
 (* gty is supposed to be meta-closed *)
 let is_subsumed depth filter_depth status gty cache =
   if cache=[] then false else (