| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
|
|
This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
|
|
We also update the plugin tutorial.
This was already tried [in the same exact way] in #8811, however the
bench time was not convincing then, but now things seem a bit better,
likely due to the removal of some extra normalization somewhere.
Some more changes from #8811 are still pending.
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Supersedes #8718.
|
|
|
|
|
|
Not sure what the right solution is here, but we can improve after the merge.
|
|
'168a13dab1c9987f592994150997e692d4d7e40b'
git-subtree-dir: doc/plugin_tutorial
git-subtree-mainline: 8c040974facb733682d24c488dc89941671f4ab7
git-subtree-split: 168a13dab1c9987f592994150997e692d4d7e40b
|
