...

[helm.git] / helm / software / components / ng_tactics / nnAuto.ml

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 39eb0baac01ac22eb6d0c480fba01b315233370e..c1b5c302f2b5a27147eff1c629c4558fca12f516 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1662,7 +1662,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,6 +1734,7 @@ 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