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 /doc/plugin_tutorial/tuto1/src | |
| 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 'doc/plugin_tutorial/tuto1/src')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 75251d8e33..147b0df567 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -146,11 +146,12 @@ END VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof ] [ "Cmd9" ] -> - { fun ~pstate -> - Option.iter (fun (pstate : Proof_global.t) -> + { fun ~pstate:ontop -> + Option.iter (fun ontop -> + let pstate = Proof_global.get_current_pstate ontop in let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate; - pstate } + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop; + ontop } END |