diff options
| author | Gaëtan Gilbert | 2019-05-02 19:46:02 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 8abacf00c6c39ec98085d531737d18edc9c19b2a (patch) | |
| tree | 52127cb4b3909e94e53996cd9e170de1f2ea6726 /proofs/pfedit.ml | |
| parent | 1c228b648cb1755cad3ec1f38690110d6fe14bc5 (diff) | |
Proof_global: pass only 1 pstate when we don't want the proof stack
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7333114eae..66b47a64a7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) -let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) +let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) (**********************************************************************) (* Shortcut to build a term using tactics *) @@ -121,7 +121,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let evd = Evd.from_ctx ctx in let terminator = Proof_global.make_terminator (fun _ -> ()) in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~ontop:None evd id goal_kind goals terminator in + let pf = Proof_global.start_proof evd id goal_kind goals terminator in try let pf, status = by tac pf in let open Proof_global in |