From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 18 Nov 2011 16:04:58 +0000 (+0000)
Subject: Solves a bug that caused the auto statistics to refer to objects that are not
X-Git-Tag: make_still_working~2081
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4db1d6f4484eb6615bffc045078b0aded277d45a;p=helm.git

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 572cd4e28..32573639b 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