Solves a bug that caused the auto statistics to refer to objects that are not

loaded in the environment, forcing them to be loaded and causing all sorts of
problems.

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 572cd4e28932d25c1bf1ed119ade0c8a4fd95bb5..32573639b350a11d591e23cecdd5bf42003a433c 100644 (file)
--- 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