| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.
More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast
in a pattern is not a fatal error.
We move this check to the internalization function, which is the
logical place to raise it, removing a bit boilerplate code.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
|
| |/ / |
|
| | | |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | | |
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
| | | | |
| | | |
| | | |
| | | | |
A priori considered to be a good programming style.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
let-ins
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
|/| | | |
|
| | | | | |
|
| |\ \ \ \
| | |_|/
| |/| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.
Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Emilio Jesus Gallego Arias
Gaetan Gilbert
Matej Kosik