X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7a9c20f0f85ce0b6106db7819162bf470c9d9793;hb=8bbe582d87984526f40182c4409cbfd43108cb79;hp=39eb0baac01ac22eb6d0c480fba01b315233370e;hpb=5f2a4177ea8f13e2f854cf64e36e1b24e9f001bd;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 39eb0baac..7a9c20f0f 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -578,6 +578,8 @@ let smart_apply t unit_eq status g =
         debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
         fast_eq_check unit_eq status j
     with
+      | NCicEnvironment.ObjectNotFound s as e ->
+          raise (Error (lazy "eq_coerc non yet defined",Some e))
       | Error _ as e -> debug_print (lazy "error"); raise e
 
 let smart_apply_tac t s =
@@ -1662,7 +1664,7 @@ let cleanup_trace s trace =
 	    | _ -> false) trace
 ;;
 
-let auto_tac ~params:(univ,flags) status =
+let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
   let oldstatus = status in
   let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
@@ -1734,10 +1736,11 @@ let auto_tac ~params:(univ,flags) status =
                   | _ -> assert false
               in
               let s = s#set_stack stack in
+                trace_ref := trace;
                 oldstatus#set_status s 
   in
   let s = up_to depth depth in
-    print (print_stat statistics);
+    debug_print (print_stat statistics);
     debug_print(lazy
         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
     debug_print(lazy