| Age | Commit message (Collapse) | Author |
|---|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
the intros tactic to its own subsection. Add grammar and examples.
|
|
|
|
|
|
This is for consistency with "rewrite {x..} y"
|
|
|
|
|
|
|
|
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
|
|
This is slightly blunt, it might be the case that we get delayed constraints
that cannot be solved resulting in a later universe inconsistency, but it looks
highly unlikely on arithmetical statements.
Alternatively we would have threaded the unification state, but this would
have required a much deeper change.
Fixes #9268.
|
|
This commit fixes a leftover of the merge of ssrmatching where
the .ml code received the appropriate banner, while the .v and
.mli di dnot.
|
|
|
|
|
|
|
|
(in case of side effects)
Also:
Fix #4781
Fix #4496
|
|
|
|
The warning can be avoided with the attributes, (or just disable the
warning itself I guess).
|
|
|
|
|
|
This commit implements the following intro patterns:
Temporary "=> +"
"move=> + stuff" ==== "move=> tmp stuff; move: tmp"
It preserves the original name.
"=>" can be chained to force generalization as in
"move=> + y + => x z"
Tactics as views "=> /ltac:(tactic)"
Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
Limited to views on the right of "=>", views that decorate a tactic
as move or case are not supported to be tactics.
Dependent "=> >H"
move=> >H ===== move=> ???? H, with enough ? to
name H the first non-dependent assumption (LHS of the first arrow).
TC isntances are skipped.
Block intro "=> [^ H] [^~ H]"
after "case" or "elim" or "elim/v" it introduces in one go
all new assumptions coming from the eliminations. The names are
picked from the inductive type declaration or the elimination principle
"v" in "elim/v" and are appended/prepended the seed "H"
The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).
|
|
|
|
workers
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
This should improve correctness and will be needed for the PRs that
remove global access to the proof state.
|
|
|
|
|
|
|
|
|
|
|
|
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
Also remove a few undocumented settings
|
|
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
|
|
|
|
|
|
|
|
As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
|
|
|
|
Users can now register string notations for custom inductives.
Much of the code and documentation was copied from numeral notations.
I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.
Some choices about proofs of the new `byte` type were made based on
efficiency. For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast. (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)
In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).
There is unfortunately a decent amount of code duplication between
numeral notations and string notations.
I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.
Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type. This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type. (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)
N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.
Closes #8853
|
|
We remove a few aliases present in the lower layers
[`Genintern/Tactypes`] from `Tacexpr`.
IMHO this enlarges the API for no good purpose, and difficults
analysis.
|
|
- remove duplicate type definitions `gram_assoc`, `gram_position`,
- make global `warning_verbose` variable into a parameter.
|
|
write_function
|
|
|
|
This is needed in order to serialize ssreflect programs properly,
similar to #6795.
|
|
|
|
|
|
|
