| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
notations in patterns
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: LasseBlaauwbroek
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
Using it feels nicer this way, with GADT details hidden inside comtactic
|
|
We move quite a few obligation functions from a `let rec ... and`
block, as they are not mutually recursive.
By the way, we perform some refactoring on `solve_by_tac`, which is
quite messy still, but now the code flow could actually accommodate
passing a declaration entry instead of low-level objects.
[It seems that we will need to introduce a special obligation entry
for that purpose, but thankfully it will be internal. We are actually
pretty close on being able to remove `build_by_tactic`, which we
should do ASAP due to its current semantics breaking abstraction
barriers]
|
|
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
|
|
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
|
|
Reviewed-by: ppedrot
|
|
We don't give sense to pattern/binders in leftmost position.
|
|
We prevent notations involving binders (i.e. names or patterns) to be
used for printing in "match" patterns. The computation is done in
"has_no_binders_type", controlling uninterpretation.
|
|
Fixes implicit arguments from the body of a defined field not taken into account.
Get (a bit) more information for detection of SProp relevance in
implicitly-typed defined field. (It should be done at the very end of
the inference phase, though, because some evars may not yet be
instantiated.)
|
|
This shall be for Record fields consumption.
|
|
Reviewed-by: herbelin
Ack-by: SkySkimmer
|
