| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
|
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
|
|
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
|
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
|
|
|
|
|
|
|
|
Mostly documentation and making a couple of local flags, local.
|
|
record fields.
|
|
Note: Apparently not easy to make a test file as the error is raised
in "G_vernac.fresh_var" at parsing time (not captured by Fail).
|
|
|
|
|
|
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
|
|
This is a bit long, but it is to keep a symmetry with constr_expr.
|
|
|
|
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).
|
|
|
|
Note: This reveals a little bug yet to fix in g_vernac.ml4. In
Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.
the "id" are wrongly unfolded and in
Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.
an unexpected cast remains in the body of f.
|
|
Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.
Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.
So, there is also a "fix" of semantic here.
|
|
No functional change.
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
|
|
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.
|
|
|
|
|
|
Type annotations in unrelated binders were badly interfering with
detection of recursive binders in notations.
|
|
The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:
https://en.wikipedia.org/wiki/Lambda_lifting
|
|
|
|
|
