| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
specific format.
Reviewed-by: ejgallego
|
|
-> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
|
|
|
|
It was not documented, not properly tested and thus likely buggy. Judging
from the code alone I spotted already one potential bug. Further more it was
prominently making use of the infamous "arbitrary term as hint" feature.
Since the only user in our CI seems to be a math-classes file that introduced
the feature under a claim of "cleanup", I believe we can safely remove it
without anyone noticing.
|
|
lonely notation at printing time.
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
quotations at printing time
Reviewed-by: ppedrot
|
|
applications in notations
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
|
|
We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.
|
|
We arbitrarily use max_int as higher level of custom entries in
printing, which should be ok since only < and <= are used to decide
when to use coercions.
|
|
Keep Numeral Notation wit a deprecation warning.
|
|
|
|
Fix #12887
|
|
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
|
|
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
|
|
That is, in "About", use _ for the variables of the extra lists.
See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
|
|
validated.
|
|
|
|
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 [ ].
|
|
|
|
Fix (partial) #5502
|
|
arguments of notations
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
Reviewed-by: Zimmi48
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
be added
Reviewed-by: CohenCyril
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
When calling an Ltac function, add specific locations when
interpreting the function, when interpreting the arguments and when
executating the call (in a TacArg).
|
|
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`.
|
|
The update of a loc needs sometimes to override (when calling an Ltac
function), and otherwise to keep the existing loc (assumed to be
fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests).
Moreover, when overriding, this was going to a tclOR backtracking
point which was setting the loc to a completely disjoint part of the
code having caused the error (see #12773). We replace the tclOR by a
tclORELSE.
|
|
|
|
generic printing format in anticipation of further not-only-parsing uses of the notation
Reviewed-by: ppedrot
|
|
asked to be printed as themselves
Reviewed-by: SkySkimmer
|
|
This was already the case for constant, but not for constructors and
inductive types.
For instance, in message "The constructor @cons (in type list) is
expected to ..." we don't want a @ to be printed.
|
|
This is to anticipate further not-only-parsing uses of the notation.
|
|
A special case for recursive n-ary applications was missing when the
head of the application was a reference.
|
|
|
|
|
