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).

14 files changed, 41 insertions, 25 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5cd34038f..6cd56e6a6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -350,7 +350,7 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of goal_selector * raw_tactic_expr * bool
+  | VernacSolve of goal_selector * int option * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8655983c4..a6eefd375 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 ] ]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b6ab7a238..466606a9b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -771,14 +771,20 @@ let rec pr_vernac = function
       hov 2 (str"Include" ++ spc() ++
 	     prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
   (* Solving *)
-  | VernacSolve (i,tac,deftac) ->
+  | VernacSolve (i,info,tac,deftac) ->
       let pr_goal_selector = function
         | SelectNth i -> int i ++ str":"
         | SelectId id -> pr_id id ++ str":"
         | SelectAll -> str"all" ++ str":"
         | SelectAllParallel -> str"par"
       in
+      let pr_info =
+        match info with
+        | None -> mt ()
+        | Some i -> str"Info"++spc()++int i++spc()
+      in
       (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
+      pr_info ++
       pr_raw_tactic tac
       ++ (if deftac then str ".." else mt ())
   | VernacSolveExistential (i,c) ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b96a12c46..c5eb03d5f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -31,7 +31,7 @@ let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
-    | None -> p,true
+    | None -> p,(true,[])
     | Some tac -> Proof.run_tactic env tac p))
 
 let cook_this_proof p =
@@ -87,7 +87,7 @@ let current_proof_statement () =
     | (id,([concl],strength)) -> id,strength,concl
     | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
 
-let solve ?with_end_tac gi tac pr =
+let solve ?with_end_tac gi info_lvl tac pr =
   try 
     let tac = match with_end_tac with
       | None -> tac
@@ -99,7 +99,13 @@ let solve ?with_end_tac gi tac pr =
       | Vernacexpr.SelectAllParallel ->
           Errors.anomaly(str"SelectAllParallel not handled by Stm")
     in
-    Proof.run_tactic (Global.env ()) tac pr
+    let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
+    let () =
+      match info_lvl with
+      | None -> ()
+      | Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+    in
+    (p,status)
   with
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
     | CList.IndexOutOfRange ->
@@ -108,7 +114,7 @@ let solve ?with_end_tac gi tac pr =
 	                            Errors.errorlabstrm "" msg
         | _ -> assert false
 
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
 
 let instantiate_nth_evar_com n com = 
   Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d77ab667b..31e3d506b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -126,7 +126,8 @@ val get_used_variables : unit -> Context.section_context option
     proof is focused or if there is no [n]th subgoal. [solve SelectAll
     tac] applies [tac] to all subgoals. *)
 
-val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> unit Proofview.tactic ->
+val solve : ?with_end_tac:unit Proofview.tactic ->
+      Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
       Proof.proof -> Proof.proof*bool
 
 (** [by tac] applies tactic [tac] to the 1st subgoal of the current
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 1dc89ca2c..abd1024d6 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -318,7 +318,7 @@ let initial_goals p = Proofview.initial_goals p.entry
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve,give_up),_) = Proofview.apply env tac sp in
+  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply env tac sp in
   let shelf =
     let sigma = Proofview.return tacticced_proofview in
     let pre_shelf = pr.shelf@(List.rev (Evd.future_goals sigma))@to_shelve in
@@ -327,7 +327,7 @@ let run_tactic env tac pr =
   in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals tacticced_proofview in
-  { pr with proofview ; shelf ; given_up },status
+  { pr with proofview ; shelf ; given_up },(status,info_trace)
 
 (*** Commands ***)
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1112a26c6..be23d7729 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -163,7 +163,8 @@ val no_focused_goal : proof -> bool
 
 (* the returned boolean signal whether an unsafe tactic has been
    used. In which case it is [false]. *)
-val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool
+val run_tactic : Environ.env ->
+  unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree)
 
 val maximal_unfocus : 'a focus_kind -> proof -> proof
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 1994922a9..4000db47c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -149,12 +149,11 @@ let with_current_proof f =
         match p.endline_tactic with
         | None -> Proofview.tclUNIT ()
         | Some tac -> !interp_tac tac in
-      let (newpr,status) = f et p.proof in
+      let (newpr,ret) = f et p.proof in
       let p = { p with proof = newpr } in
       pstates := p :: rest;
-      status
-let simple_with_current_proof f =
-  ignore (with_current_proof (fun t p -> f t p , true))
+      ret
+let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
 
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index b0e53ecd8..de259a4cc 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -114,7 +114,7 @@ val get_open_goals : unit -> int
     no current proof.
     The return boolean is set to [false] if an unsafe tactic has been used. *)
 val with_current_proof :
-  (unit Proofview.tactic -> Proof.proof -> Proof.proof*bool) -> bool
+  (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a
 val simple_with_current_proof :
   (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bf4a1e5a6..d55689a20 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -967,7 +967,9 @@ module Trace = struct
   let log m = InfoL.leaf (Info.Msg m)
   let name_tactic m t = InfoL.tag (Info.Tactic m) t
 
-  let pr_info = Info.print
+  let pr_info ?(lvl=0) info =
+    assert (lvl >= 0);
+    Info.(print (collapse lvl info))
 
 end
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 934a44574..cc8706ab2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -482,7 +482,7 @@ module Trace : sig
   val log : Proofview_monad.lazy_msg -> unit tactic
   val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
 
-  val pr_info : Proofview_monad.Info.tree -> Pp.std_ppcmds
+  val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds
 
 end
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 4b4d50c41..b72b5bb2a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1125,7 +1125,7 @@ module Partac = struct
 
   let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
     let e, etac, time, fail =
-      let rec find time fail = function VernacSolve(_,re,b) -> re, b, time, fail
+      let rec find time fail = function VernacSolve(_,_,re,b) -> re, b, time, fail
         | VernacTime [_,e] -> find true fail e
         | VernacFail e -> find time true e
         | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
@@ -1137,7 +1137,7 @@ module Partac = struct
       let open SubTask in
       let res = CList.map_i (fun i g ->
         let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in
-        let t_ast = { verbose;loc;expr = VernacSolve(SelectNth i,e,etac) } in
+        let t_ast = { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task
           { t_state = safe_id; t_state_fb = id;
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 733f3e441..63b9e2e7f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -97,7 +97,7 @@ let rec classify_vernac e =
     | VernacCheckMayEval _ ->
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
-    | VernacSolve (SelectAllParallel,_,_) -> VtProofStep true, VtLater
+    | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
     | VernacProof _ 
     | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb50a6bc2..af7d2a723 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -800,14 +800,14 @@ let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
 
-let vernac_solve n tcom b =
+let vernac_solve n info tcom b =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
   let status = Proof_global.with_current_proof (fun etac p ->
     let with_end_tac = if b then Some etac else None in
     let global = match n with SelectAll -> true | _ -> false in
     let (p,status) =
-      solve n (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+      solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
     in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
@@ -1827,7 +1827,7 @@ let interp ?proof locality poly c =
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
-  | VernacSolve (n,tac,b) -> vernac_solve n tac b
+  | VernacSolve (n,info,tac,b) -> vernac_solve n info tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)