Add [Info] command.

Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).

1 files changed, 3 insertions, 2 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8655983c4b..a6eefd3755 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -152,11 +152,12 @@ GEXTEND Gram
                     | _ ->
                         VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
                   end
-      | tac = Tactic.tactic;
+      | info = OPT [IDENT "Info";n=natural -> n];
+        tac = Tactic.tactic;
         use_dft_tac = [ "." -> false | "..." -> true ] ->
         (fun g ->
             let g = Option.default (Proof_global.get_default_goal_selector ()) g in
-            VernacSolve(g,tac,use_dft_tac)) ] ]
+            VernacSolve(g,info,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
     [ [ v = vernac -> !@loc, v ] ]