diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 17:55:48 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-01 22:43:57 +0100 |
| commit | 967883e29a46a0fff9da8e56974468531948b174 (patch) | |
| tree | 9c9a814a92c2a7fb5006d478e6d20e16bcf74d7a /proofs/pfedit.ml | |
| parent | 3c8797a7e0d6536e28b8a8e7f4256241fc79dfc8 (diff) | |
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).
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 14 |
1 files changed, 10 insertions, 4 deletions
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) |