| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
| |
We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
|
| |\ |
|
| | |
| |
| |
| |
| | |
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
|
| | |\ |
|
| |\ \ \
| | |/
| |/| |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This happens when recursive notations are used to define recursive
notations.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
But maybe it is that how the "Test" message is elaborated is not
intuitive...
|
| | | | |
| | | |
| | | |
| | | | |
(It should apply also interactively.)
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
#4363)."
This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402.
This fixes bug #4874. We fallback to the original error message of v8.4.
The fallback printer introduced in this commit only gave unqualified names,
which is what this bug reports.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Enablnig them would give a system that tells the user to replace e.g.:
le_n_Sn with Nat.le_succ_diag_r
lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same
lemma is called lt_lt_succ)
In many cases, the new names will be too painful for intensive users.
|
| | | |
| | |
| | |
| | |
| | | |
These warnings can now be configured like any other, so we don't need
a specific option anymore.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We protect the code against the presence of pattern casts where they are
not supported. Why we cannot make the pattern type reflect this is
a long story (described in this commit), but in the long term we
probably want to support them anywhere, like OCaml does. Of course, it
will require to adjust the pattern matching compiler.
|
| | | |
| | |
| | |
| | | |
Also getting rid of a global side-effect.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).
This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ML side lacks a method to query Coq for notations with defined
parsing/printing rules. This commit adds a method
`get_defined_notations` to that purpose.
This is very useful for instance in plugins like SerAPI.
In the medium-term, the `Notation` interface may benefit from a bit of
refactoring to allow programmatic access and manipulation of notations.
|
| | |
| |
| |
| |
| | |
All compilation (by)products are placed where -o specifies.
Used to be the case for .vo, .vio, .aux but not .glob
|
| | | |
|
| | |
| |
| |
| | |
One of them revealed a true bug.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
consistency of the use of names.
|
| | | |
|
| | |
| |
| |
| | |
aliases.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The logic was backward: if the path of a symbol was a prefix of the
current path, then the current path (without sections) was used. But what
we want is that, if the current path (without sections) is a prefix of the
path of a symbol, then the former should be used.
This fixes about 1,600 broken links in the documentation of the standard
library.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- typo in notation_ops.ml
- factorization of patterns in ppconstr.ml
- update of test-suite
- printing of cast of a binding pattern if in mode "printing all"
The question of whether or not to print the type of a binding pattern
by default seems open to me.
|
| | |
| |
| |
| |
| | |
Supporting accordingly printing of sequences of binders including binding
patterns.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The same variable name was used to collect the binders and the
successive steps of matching one binder, resulting in unexpected
attempts for merging in the presence of multiple occurrence of the
same recursive pattern.
An amusing side-effect: when eta-expanding for a notation with
recursive binders, it is the second variable of the "x .. y" which is
used to invent a name rather than the first one.
|
| | |
| |
| |
| |
| |
| |
| | |
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
|
| | | |
|
| | |
| |
| |
| | |
immediately in the scope of another recursive pattern.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
In particular, it becomes possible to have recursive patterns used
shared by binders and terms.
Currently limited by alpha-conversion issues (e.g. test2 from 4932.v
is not reprinted).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This application was actually not anticipated. It is nice and was not
too difficult to support.
Design for pattern binders maybe to clarify. When seing pat(x1,..,xn)
as a term, I just reused pat(x1,..,xn), but maybe it is worth using
the variable aliasing the pattern, for more a concise notation. But at
the same time, this means exposing the internal name of the alias
which is not so elegant.
|
| | |
| |
| |
| |
| | |
This happens when recursive notations are used to define recursive
notations.
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This maintains compatibility, it is debatable if we should use implicit
type information for lets to allow for coercions to fire.
(Problem found in math-comp).
|
| | | | |
|
| |/ /
| |
| |
| | |
They were allowing algebraic universes to slip in terms.
|
Hugo Herbelin
Pierre-Marie Pédrot
Théo Zimmermann
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Guillaume Melquiond
Matej Kosik
Matthieu Sozeau