| Age | Commit message (Collapse) | Author |
|---|
|
We introduce a class of open binders which includes "x", "x:t", "'pat"
and a class of closed binders which includes "x", "(x:t)", "'pat".
|
|
Reviewed-by: gares
|
|
an arity.
Reviewed-by: ppedrot
|
|
After the previous commit, the stm should correctly pass proof
information, thus we make `proof_object` carry it removing a bunch of
internal code.
|
|
Since 8.5, the STM could not delegate proof information it was
contained inside a closure. This could potentially create some
problems, as witnessed in #12586.
Recent refactoring have reified however much of this state, so it
seems a good idea to use bits of the state now, at the cost of
introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.
|
|
|
|
|
|
We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).
We update the documentation, test-suite, and changelog.
|
|
Following discussion in https://github.com/coq/coq/pull/12586 , we
extend the syntax `val=string` to support also arbitrary values.
In particular we support boolean ones, or arbitrary key-pair lists.
This complements the current form `val="string"`, and makes more sense
in general.
Current syntax for the boolean version is `attr=yes` or `attr=no`, but
we could be more liberal if desired.
The general new guideline is that `foo(vals)` is reserved for
the case where `vals` is a list, whereas `foo=val` is for attributes
that allow a unique assignment.
This commit only introduces the support, next commits will migrate
some attributes to this new syntax and deprecate the old versions.
|
|
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
|
|
variables.
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: SkySkimmer
|
|
Ack-by: Blaisorblade
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48
|
|
Fix #13300
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
This is a better abstraction barrier (no "symbol" type with
uninterpreted ".." exported out of notation.ml). It also allows to
"browse" notations mentioning a "..".
|
|
|
|
Fix #6042
Also introduce a deprecated compat option
|
|
Co-authored-by: <Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
We re-expose `declare_projections` and `declare_structure_entry` as it
is needed by coq-elpi.
Ideally we would provide a better way in recordops to interact with
this, in fact `declare_structure_entry` is just a wrapper around
recordops + libobject structure so there is hope it goes away entirely
in the future.
The need for Elpi to manually call `declare_projections` should
actually disappear in future refactorings.
|
|
|
|
In preparation for better handling of the regular record / class
codepath. This will also allow to pack record data better.
|
|
In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.
The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.
|
|
In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.
The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.
|
|
The IDENT annotations in g_ltac.mlg are required to not break the
parser.
|
|
"Proof with" is Ltac-specific but there is no reason why it should be
the same for "Proof using".
|
|
not only on subidentifiers of an identifier
Reviewed-by: Zimmi48
|
|
naming
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
Obligation`
Reviewed-by: SkySkimmer
|
|
Fixes #13320 .
Trivial programming error, actually this is handled better in a
further refactoring branch not submitted due to the long time the
whole rework took.
|
|
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
a correct typing environment
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
We accept patterns that we failed to type as a fallback.
|
|
|
|
|
|
Also some dead code.
If no typo is introduced, there should be no semantic changes.
|
|
We reuse the standard code path for term interpretation instead of trying
to mangle it.
|
|
The prepare_hint function was trying to requantify over all undefined evars,
but actually this should not happen when defining generic terms as hints through
some Hint vernacular command.
|
|
|
