| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main point of this change is to fix #3035: Avoiding trailing
arguments in the Arguments command, and related issues occurring in
HoTT for instance. When the "assert" flag is not specified, we now
accept prefixes of the list of arguments.
The semantics of _ w.r.t. to renaming has changed. Previously, it meant
"restore the original name inferred from the type". Now it means "don't
change the current name".
The syntax of arguments is now restricted. Modifiers like /, ! and
scopes are allowed only in the first arguments list.
We also add *a lot* of missing checks on input values and fix various
bugs.
Note that this code is still way too complex for what it does, due to
the complexity of the implicit arguments, reduction behaviors and renaming
APIs.
|
| |
|
|
|
|
| |
The patch is quite dumb: it essentially consists in alpha-renaming bound
module names when printing a functor, by checking that the name was not
already present, and generating a fresh one otherwise.
|
| |\ |
|
| | |
| |
| |
| | |
Restore subst output test file modified by mistake.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
It seems warnings are not taken into account in output/
tests.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
|
| |/ / |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| | |
| |
| |
| | |
(In agreement with Daniel.)
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Further work would include:
- Identify binders up to alpha-conversion (see #4932 with a list of
binders of length at least 2, or #4592 on printing notations such as
ex2).
A cool example that one could also consider supporting:
- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
(cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
|
| | |
| |
| |
| | |
immediately in the scope of another recursive pattern.
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Cf CHANGES for details.
|
| | | |
|
| | |
| |
| |
| |
| | |
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
| | |
| |
| |
| | |
along with goals, with nice formatting.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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}.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...
It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.
It got really bad in 8.5 as in:
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I. (* was referring to tactic name "Top.Top#<>#1" *)
which this commit fixes.
I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.
Eventually, it might be worth that an Ltac expert brainstrom on it!
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
| | | |
|
| | |
| |
| |
| | |
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
| | | |
|
| |\ \
| | |
| | |
| | | |
into JasonGross-trunk-function_scope
|
| |\ \ \
| | |/
| |/| |
|
Maxime Dénès
Pierre-Marie Pédrot
Enrico Tassi
Hugo Herbelin
Matthieu Sozeau
Paul Steckler
Arnaud Spiwack
Daniel de Rauglaudre
Guillaume Melquiond