| Age | Commit message (Collapse) | Author |
|---|
|
This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2.
|
|
This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
|
|
This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4.
|
|
This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
|
|
This reverts commit e11620ce155529c0e577304427f9b05d38e73caf.
|
|
This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc.
|
|
pr_lconstr."
This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288.
|
|
This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
|
|
definition."
This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673.
|
|
This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
|
|
This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
|
|
This reverts commit 90252e973f5bcafc5f3b0b18564612d7fb4503a8.
|
|
This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90.
|
|
This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
|
|
EXTEND and""
This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
|
|
This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
|
|
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.
|
|
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".
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
VERNAC EXTEND.
|
|
|
|
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
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.
|
|
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.
|
|
variables" when matching over "{v : _ | _ & _}" which hides twice the
binding "fun v" since it is "sig2 (fun v => _) (fun v => _)".
Computing the bound variables statically at internalisation time
rather than every time at interpretation time. This cannot hurt even
if I don't know how to deal with the "notation" problem of a single
bound variable actually hiding two: at the current time, the notation
is printed only if the two variables are identical (see #4592), so,
with this semantics the warning should not be printed, but we lost the
information that we are coming from a notation; if #4592 were
addressed, then one of the binding should be alpha-renamed if they
differ, so collision should be solved by choosing the variable name
which is not renamed, but the matching algorithm should then be aware
of what the notation printing algorithm is doing... maybe not the most
critical thing at the current time.
|
|
|
|
I made a confusion between ltac: in constr and ltac: in tactics, the
one needing parentheses in v8.5 but the latter needing parentheses
only in trunk.
This reverts commit f5dc54519f2a62bab2f7b9059e8c3c8dc53619be.
|
|
|
|
|
|
|
