| Age | Commit message (Collapse) | Author |
|---|
|
This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
|
|
This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
|
|
This reverts commit e01dabf9f7aa530c4c70aadf464097cd102b1df6.
|
|
This reverts commit 36fb3d3a53418a81675815e47b3810e11bc31e4c.
|
|
This reverts commit 84d8a4bd7d797b6e13e4107ad24a6dcf4f098dbb.
|
|
This reverts commit df1e24f64f68318221d08246098837368ee1b406.
|
|
This reverts commit 8c74d3e5578caeb5c62ba462528d9972c1de17f1.
|
|
This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4.
|
|
This reverts commit e0fd6e50800bc5aec4eafddd315941d6f7bc6efc.
|
|
This reverts commit 239f30c2070018db88e568acca6c9054f650ca38.
|
|
EXTEND and""
This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
|
|
This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
|
|
|
|
|
|
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".
|
|
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.
|
|
|
|
|
|
presence of entries starting with a non-terminal such as "b ^2".
|
|
|
|
VERNAC EXTEND.
|
|
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
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.
|
|
|
|
|
|
|
|
|
|
Instead of relying on entry names as given by a hardwired registering
scheme in Pcoq, we recover them first through a user-defined map, and
fallback on generic argument names.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This type was actually only used by the debug printer of tactics, and only
for atomic tactics. Furthermore, that type was asymmetric, as the underlying
tacexpr type was set to be glob_tactic, when the semantics would have required
a Val.t type.
Furthermore, this type is absent from every contrib I have seen, which hints
again in favour of its lack of meaning.
|
|
|
|
pr_vernac.
|
|
|
|
This is not perfect yet, in particular the whole precedence system is a real
mess, as there is a real need for tidying up the Pptactic implementation.
Nonetheless, printing toplevel values is only used for debugging purposes, where
an ugly display is better than none at all.
|
|
It was only used by setoid_ring for the Add Ring command, and was easily
replaced by a dedicated argument. Moreover, it was of no use to tactic
notations.
|
|
|
|
|
|
product in setoid_rewrite.
Before commit e8c47b652, it was raising an error which has been turned
to an anomaly.
This impacted Compcert where the former error was (apparently) caught
so that setoid_rewrite was returning back to ordinary rewrite.
|
|
|
|
|
|
|
|
|
|
|
|
|
