| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
Hugo Herbelin
Pierre-Marie Pédrot