| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Previously a union type was used for externing.
In particular, moving extended_glob_local_binder to glob_constr.ml.
|
| | | |
| | |
| | |
| | | |
RawLocal -> CLocal
|
| | | |
| | |
| | |
| | | |
No more constr_expr in it.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Aligned the type binder_data to the naming scheme used in (raw)
local_binder and Rel.Declaration.t. Made some code factorization.
Still to do: align type Glob_term.glob_binder to the Assum/Def format
too.
Note: this includes fix of anomaly with 'pat in cofix (dec77f282).
|
| | |/ |
|
| | |\ |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| | |
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| |\ \
| | |
| | |
| | | |
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| | |
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
|
| | |
| |
| |
| | |
This removes a dependency on wit_tactic in Constrintern.
|
| |\ \
| |/
|/| |
|
| | | |
|
| | |
| |
| |
| | |
Suggested by @ppedrot
|
| | |
| |
| |
| |
| |
| |
| | |
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
| |
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
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| | |
(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 = ... }.
|
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Enrico Tassi
Guillaume Melquiond
Emilio Jesus Gallego Arias
Matthieu Sozeau
Pierre Letouzey
Matthieu Sozeau
Gabriel Scherer