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

8 files changed, 24 insertions, 15 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b96a12c46d..c5eb03d5fe 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 d77ab667bc..31e3d506b8 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 1dc89ca2c6..abd1024d6e 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 1112a26c6b..be23d77296 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 1994922a97..4000db47c2 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 b0e53ecd87..de259a4cca 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 bf4a1e5a69..d55689a202 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 934a445743..cc8706ab2e 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