| Age | Commit message (Collapse) | Author |
|---|
|
Fix #6042
Also introduce a deprecated compat option
|
|
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
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Ack-by: SkySkimmer
|
|
We fix a clear coding mistake in
79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the
type of the parameter entry when saving mutual definitions without a
body.
We follow the solution suggested by Hugo Herbelin and drop the
type used in `start_proof`. Note the duplication here indeed.
Fixes #12895
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
Fix #13162
|
|
This improves the error message on the example for #13171, however we
may question whether there should be an error at all.
|
|
|
|
The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.
Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.
The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.
Additionally, we anticipate the ability to selectively
activate/deactivate each of those.
This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.
Rules for importing are not changed (see forthcoming #12984 though).
We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.
Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
|
|
This is to be consistent with the use of parentheses in the syntax of
Notation and to support a list of attribute afterwards.
|
|
|
