From 4db1d6f4484eb6615bffc045078b0aded277d45a Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 18 Nov 2011 16:04:58 +0000 Subject: [PATCH] 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. --- matita/components/ng_tactics/nnAuto.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -- 2.39.2