| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
with a more explicit message.
|
|
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
|
This was only when compiling with Camlp4 and it was producing an
assertion failure in asmcomp/emitaux.ml at line 226, reported as
OCaml's bug #6243.
Note: The issue of a problematic compilation with 4.01.0 was raised at
last WG.
|
|
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.
|
|
Bug uncovered by ekcburak@hotmail.com
https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00006.html
Now, terms of the the form (Rinv t) are only syntaxified when t evaluates to a non-zero constant.
|
|
The documentation of Ocaml's `Format` module specifies:
> The behaviour of pretty-printing commands is unspecified if there is
> no opened pretty-printing box. Each box opened via one of the open_
> functions below must be closed using close_box for proper
> formatting. Otherwise, some of the material printed in the boxes may
> not be output, or may be formatted incorrectly.
(http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html)
However, [lib/pp.ml] seems not to take lots of precautions to ensure
that format is always called with an enclosing box.
If `log_via_feedback` is set, [lib/pp.ml:string_of_ppcmds] will call
`msg_with` without a top-level enclosing box, resulting in poor display
results like mismatched width.
Note that there are more functions affected, but these codepaths don't
seem to matter when `log_via_feedback` is set.
A small cleanup of pp.ml may be in order.
|
|
so that they are not silently computed when not in debugging mode.
|
|
|
|
|
|
|
|
Will be displayed on the website, but not part of the package.
|
|
computed when not in debugging mode (especially those printing a
command).
|
|
|
|
|
|
in file indtypes.ml so that it is easier to follow what the code is
doing.
This is a purely alpha-renaming commit (if no mistakes).
Note: was submitted as pull request #116.
|
|
|
|
Most notably, we bring the single argument and three argument variants
closer, so that the various TYPED AS clauses may be optional. Compile-time
warnings have been added for redundant clauses.
|
|
|
|
|
|
|
|
|
|
|
|
The TYPED AS clause was useless when defining a fresh generic argument.
Instead of having to write it mandatorily, we simply make it optional.
|
|
This allows to use the ARGUMENT EXTEND macro while sharing the same
toplevel dynamic representation as another argument.
|
|
location set by lexer). This improves on abb4e7b0c by recovering the
lexer location.
AFAICS, it has an effect on lexer's errors Unterminated_comment and
Unterminated_string. The other errors were not wrongly located,
presumably because the Exc_located location added by camlp5 coincided
with the location given by the lexer.
|
|
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
hintbases so that it does not put extra space when auto is defined as
a TACTIC EXTEND.
|
|
pr_vernac.
|
|
|
|
|
|
be used in the generic printer for tactics.
Allows e.g. to print "symmetry in H" correctly after its move to
TACTIC EXTEND.
|
|
|
|
The extraction of [Z] into Ocaml's [Big_int] passed arguments in the
wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems
unlikely this ever worked before.
|
|
|
|
printer in the congruence tactic.
Debugging messages were always built even when not in the verbose mode
of congruence.
|
|
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.
|
