| Age | Commit message (Collapse) | Author |
|---|
|
![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`
The other specifiers are for the following body types:
~~~
![open_proof] `is_ontop:bool -> pstate`
![maybe_open_proof] `is_ontop:bool -> pstate option`
![proof] `pstate:pstate -> pstate`
![proof_opt_query] `pstate:pstate option -> unit`
![proof_query] `pstate:pstate -> unit`
~~~
The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.
The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.
![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
don't fully understand, maybe we can drop it in the future.
For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
|
|
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.
|
|
|
|
|
|
'168a13dab1c9987f592994150997e692d4d7e40b'
git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b
|
