| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: herbelin
|
|
notations in patterns
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: LasseBlaauwbroek
|
|
|
|
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.
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
|
|
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.
|
|
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
|
|
time and use location in some typing error messages
Reviewed-by: ppedrot
|
|
|
|
|
|
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
|
|
Also add optimisation of interpretation_eq.
|
|
|
|
missing.
|
|
|
|
Fix #13117
We alternatively could fix the generation of the data with Existing
Class but I prefer moving towards removing it.
|
|
|
|
Used only by implicit_quantifiers
|
|
Fix #13131
|
|
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
|
|
lonely notation at printing time.
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
applications in notations
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
|
|
The bugs involved:
- a notation with a subterm in position of function of an application
- use of this notation in another notation creating a non-flattened application
In particular, this fooled "find_appl_head" (for #10803) and the
translation from GApp to NApp (for #9403).
We fix the translation NApp -> GApp (since glob_constr is supposed to
have its applications flattened).
|
|
Strangely, this was not yet noticed. Hiding of a scoped notation by a
lonely notation should be checked at printing time.
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
renaming.
Example:
> Arguments id [B] {b} : rename.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Argument B is a trailing implicit, so it can't be declared non
maximal. Please use { } instead of [ ].
|
|
Suggested by Pierre Roux
|
|
We could still optimize the functions in that file a bit more if there
is need.
|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
arguments of notations
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
|
|
n-ary applications used with applied references
Reviewed-by: ejgallego
|
|
Reviewed-by: herbelin
|
|
A special case for recursive n-ary applications was missing when the
head of the application was a reference.
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
We interpret `{|proj=pat|}` as `@C _ pat` instead of `C _ pat` (where
the `_` stands for the parameters).
Fix #12534
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
