| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
explain more
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Ack-by: tlringer
|
|
Reviewed-by: ejgallego
Ack-by: gares
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: vbgl
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
I updated the readme example using the most recent overlay with only 1
touched development.
|
|
Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: gares
|
|
Ack-by: andreaslyn
Reviewed-by: gares
|
|
|
|
AFAICT the stm never gives Load a non-None ?proof.
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
|
|
This provides uniformity to the inner loop and prepares the way to
export a refined type for interpretation.
The only non-uniformity remaining is the one due to the `?proof`
parameter; it won't be easy to fix due to upper layers issues.
Note that this step is not yet fully satisfying, as a true typed
`vernac_expr` definition is still not possible because of syntactic
non-uniformity, in particular all the surgery done for `CoFixpoint`
and `Instance` should be eliminated in favor of more refined AST tags.
An interesting TODO is to handle attributes symbolically too, as to
remove boilerplate.
|
|
|
|
Reviewed-by: mattam82
|
|
|
|
|
|
deprecated attribute
This code was significantly more complex than necessary.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
+ hide interp_functional_vernac in vernacentries
|
|
|
|
The only use of ModifyProofStack was in paramcoq for closing a proof.
|
|
|
|
|
|
|
|
|
|
eg ![proof] becomes STATE proof
This commits still supports the old ![]
so there is redundancy:
~~~
VERNAC EXTEND Foo STATE proof
| ...
VERNAC EXTEND Foo
| ![proof] ...
~~~
with the ![] form being local to the rule and the STATE form
applying to the whole EXTEND except for the rules with a ![].
|
|
![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.
|
|
Since the introduction of delayed section substitution, the opaque table
was already containing the same information.
|
|
This will allow an easier removal of the discharge segment in a later
commit.
|
|
Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
|
|
Reviewed-by: gares
Ack-by: ppedrot
|
|
|
|
Not needed since we don't allow anonymous Declare Instance
anymore (was needed for factorization or some such before that I think)
|
|
We never use this id in rewrite.ml so don't bother threading it around.
|
|
|
