| 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.
|
|
|
|
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.
|
|
keeping with doc recommendations
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
proof diffs
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Ack-by: erikmd
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Cooking
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: gares
|
|
Ack-by: RalfJung
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
|
|
They are supposed to be included in the module's constraints.
The old behaviour would allow a crafted vo, using
~~~coq
Definition a := Type.
Definition b := Type.
Definition b_in_a : a := b.
Definition a_in_b : b := a.
~~~
with the constraints for b_in_a and a_in_b not included in the module
constraints, then a proof of false may be derived in the usual way.
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
|
|
Reviewed-by: gares
Ack-by: maximedenes
|
|
We use the right environment.
|
|
For now this is just a specialized version of the previous generic code.
This simplifies tracking of the changes.
|
|
It is guaranteed by Declare, but a little dynamic check does not hurt.
|
|
The only lawbreaker was the Add Ring command. We generate a type for
the declaration to fix the code.
|
|
The idea is that it's unlikely for only 1 of the test suite copies to
fail for a real reason, so we don't need to run all of them.
I would prefer to have only 1 build stage job but later stages depend
on build:base, build:edge+flambda and build:edge+flambda:dune:dev for
non-copy-pasted jobs.
I kept corresponding test suite and validate job copies but they could
also be filtered.
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: gares
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
|
|
This is the intended module for the feature provided by the inductive
discharge. This allows for a bit of code sharing and cleanup.
|
|
|
|
|
|
options rather than files
Reviewed-by: ejgallego
|
|
patn]".
Reviewed-by: Zimmi48
|
|
than files.
|
