| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
need at matching time rather than eagerly at the beginning of the call
to "match".
To be done for other constructs too, e.g. "match term with ... endp".
|
|
|
|
|
|
fix au revert [||]
|
|
arguments of vernac extensions, so that in list with a separator, the
separator is printed.
|
|
side of Ltac's "let ... in ..." or "match ... with ... => ... end".
Example:
Ltac f x := let x := 0 in constr:(S x).
Print Ltac f.
has a missing "constr:".
Note: for generic arguments: "ltac:" is always used, even if a constr, etc.
|
|
"exists c1, c2".
|
|
the remaining issue with the fix to #3709.
However, this does not solve the problem in mind which is that
"intuition idtac; idtac" is printed with extra parentheses into
"intuition (idtac; idtac)".
If one change the level of printing of TacArg of Tacexp from latom to
inherited, this breaks elsewhere, with "let x := (simpl) in idtac"
printed "let x := simpl in idtac".
|
|
subentry at a higher tactic level than the entry itself.
This is applicable to the parsing of expressions with infix or postfix
operators such as ; or ||.
Could be improved, e.g. so that no parenthesis are put when the
expression is the rightmost one, as in:
now (tac1;tac2)
where parentheses are not needed but still printed with this patch,
while the patch adds needed parentheses in
(now tac1);tac2
This would hardly scale to more complex grammars. E.g., if a suffix
expression can extend a leading expression as part of different
grammar entries, as in
let x := simpl in y ...
I don't see in general how to anticipate the need for parentheses
without restarting the parser to check the reversibility of the
printing.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
No other changes (long only because of a change of indentation).
|
|
|
|
Fixing : in Declare Module.
|
|
|
|
|
|
|
|
|
|
|
|
"|]"" because this commit triggers a
Error: Files proofs/proofs.cma(Miscprint)
and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer)
make inconsistent assumptions over interface Lexer
Adding two extra spaces systematically instead.
This reverts commit 72be1f6beafafc3edd30df673fbb6c7e88f8fac7.
|
|
with user-level notations by inserting spaces.
|
|
exist as a keyword by inserting a space inbetween.
|
|
presence of entries starting with a non-terminal such as "b ^2".
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
implicit is found whether one writes (sig P) or {x|P x}.
|
|
VERNAC EXTEND.
|
|
|
|
implicit arguments when in beautification mode.
|
|
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
does not print to ** which is a keyword.
|
|
calling Pcoq.parse_string, what some plugins such as coretactics, are
doing, thus breaking the beautification of "Declare ML Module").
|
|
with a clause where, nor Notation, nor Fixpoints.
Should be certainly improved at least for Inductive types and
Fixpoints, depending on whether there is a "where" clause for
instance.
|
|
beautification of the standard library.
Currently not intrusive but needs two extra phases of compilation.
|
|
|
|
computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.
|
|
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.
|
|
clause of a "match" over an irrefutable pattern.
|
|
in interning of patterns.
No semantic changes (except the type of ids_of_cases_indtype).
|
