| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict
match to an hypothesis or the conclusion, possibly only at the head
(like SearchHead in this latter case)
- new clause "is:" to search by kind of object (for some list of kinds)
- support for any combination of negations, disjunctions and conjunctions,
using a syntax close to that of intropatterns.
|
|
implicit types
Reviewed-by: ejgallego
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
runtime.
Reviewed-by: herbelin
|
