| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This will allow for instance to check the status of a variable name
used both as a term and binder in notations.
|
|
Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.
We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.
Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
As noted by Hugo Herbelin, Dec is rather used for "decidable".
|
|
Until now, declaring a number or string notation on some trigger
removed all previous notations on the same scope.
Bug discovered by Jason Gross while reviewing #12218.
|
|
|
|
|
|
This will enable to handle implicit arguments by ignoring them during
preprocessing (before uninterpreting (i.e., printing)) and remplace
them with holes `_` during postprocessing (after interpreting (i.e.,
parsing)).
|
|
This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
|
|
|
|
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
|
|
|
