diff options
| author | Pierre-Marie Pédrot | 2019-05-14 23:21:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 23:21:34 +0200 |
| commit | 2a60906dd9d295615bcfa4b1fce8cea9626d965f (patch) | |
| tree | 5681d71e2cd4c038fcff690dfbc3f9d3f994bb87 /vernac | |
| parent | 75262c3f8af195a83673ff06a53d0fd0bd23b57e (diff) | |
| parent | 06b60655b98580baab98f35f6c89716e2381934c (diff) | |
Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..2dae0ad125 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -395,10 +395,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate, _ = Proof_global.with_current_proof (fun _ p -> + let pstate = Proof_global.simple_with_current_proof (fun _ p -> match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in + | None -> p + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in pstate let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = |