| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
| | |
| |
| |
| | |
more cleanups
|
| |/
|
|
| |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | |
| |
| |
| | |
See 4865.v for details.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| | | |
|
| | |
| |
| |
| | |
They can apply to the head reference under a notation.
|
| | |
| |
| |
| |
| |
| | |
internalization.
Patch by PMP, test-suite fix by MS.
|
| |\ \
| | |
| | |
| | | |
Was PR#223: Allow feedback messages to carry a location.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
(Because the function is private to the module, it is documented in
the .ml rather than the .mli)
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The type of the user-defined function "completer" changes to be
simpler and better reflect its purpose: provide values for missing
field assignments. In the future we may want to also pass the name of
the field as parameter (currently only the index is given, and both
uses of the function ignore it), in particular if we want to implement
{ r with x = ...; y = ... }.
|
| | | |
| | |
| | |
| | |
| | | |
The internal `add_pat` function is replaced by a call to
`CList.extract_first`.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The code was a big "try..with" defining all useful quantities at
once. I tried to lift definitions out of this try..with to define them
as early as possible: the record's information and the first field
name are fetched before processing the other fields.
There were two calls in the try..with body that could raise the
Not_found exception (or at least I don't know the code well enough to
be sure that either of them cannot): `shortest_qualid_of_global` and
`build_patt`. They are now split in two separate try..with blocks,
both raising the same exception (with a shared error message named
`env_error_msg`). Someone familiar with the invariants at play could
probably remove one of the two blocks, streamlining the code even
further.
I'm a bit surprised by the main logic part (the big (if .. else if
.. else if ..) block in the new code), and there is a question in
a comment. I hope to get it answered during code review and remove it
(and maybe simplify the code).
Finally, there was an apparently-stale comment in the code:
(* insertion of Constextern.reference_global *)
of course Constextern.reference_global corresponds to now function
that I could find. After trying to understand the meaning of this
comment, I decided to just remove it.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Note that turning
let boolean = not regular in
if boolean && complete then ...;
if boolean && complete then ...;
into
if not regular && complete then ...;
if not regular && complete then ...;
has absolutely no performance cost: negation inside a conditional is
not computed as a boolean, it only flips the branches. The code is
more readable because "boolean" was a terrible variable name.
|
| | | |
| | |
| | |
| | | |
Cf CHANGES for details.
|
| |/ /
| |
| |
| |
| |
| |
| |
| | |
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
| | | |
|
| | |
| |
| |
| |
| | |
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
| | |
| |
| |
| | |
implicit arguments when in beautification mode.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.
For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _",
the same way as if we had said:
Arguments eq_refl {A} {x}.
|
| |\ \ |
|
| |\ \ \
| | |/
| |/| |
|
Matej Kosik
Matej Kosik
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Matthieu Sozeau
Gabriel Scherer
Daniel de Rauglaudre
Emilio Jesus Gallego Arias