| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
printing/Ppannotation: Define the projection of annotations into XML attributes.
lib/richPp: Implements valid entities escaping.
|
|
Allow strings of a pretty-print to be rewritten just before the
actual output.
|
|
|
|
applied, to preserve previous behaviors.
|
|
|
|
|
|
|
|
internal and external datatypes.
|
|
{Interface} instead.
|
|
- Extend the protocol with a new command called "annotate".
- By the way, relax the dependencies between the "ide" package
and the internal packages of Coq by *not* referring to external
type definitions inside Interface.
Indeed, the purpose of the protocol is to act as a barrier
between the source tree of Coq and the source tree of Coqide.
We should enforce this property.
(Maybe one day coqide will be extracted from the source tree
of Coq to live its own life.)
|
|
Ppconstr: Fix a typo in comments.
|
|
Ppvernac.RichPp: New rich pretty-printer.
|
|
- Define the signature for a pretty-printer of vernacular commands.
Ppvernac: Use it.
|
|
- Ppvernac is now functorized with respect to
a Ppconstr printer.
- Preserve previous behavior by instantiating this functor
with Ppconstr.
|
|
|
|
Define the annotations stored in semi-structured pretty-prints.
Ppconstrsig: New.
Contains the signature of a pretty-printer for ppconstr.
Ppconstr: Export a new rich pretty-printer for constr_expr and co.
|
|
It is responsible for turning a tagged pretty-printing into
a semi-structured document.
clib.mllib: Include RichPp as well as Xml_*.
The migration of Xml_* from lib to clib is needed by RichPp
depends on these modules.
|
|
Xml_parser, Xml_printer: Use it.
|
|
|
|
- Functorize Ppconstr with respect to a set of tagging functions.
- These functions are meant to introduce tags to produce semistructured
pretty printings.
printing/Ppconstr:
Preserve the previous behaviour of this module by instantiating Make
with tagging functions that do nothing.
|
|
Extend this type with Ppcmd_open_tag and Ppcmd_close_tag.
lib/Pp.ppcmd_pp_dirs:
Handle these tags with a straightforward translation to
corresponding Format commands.
|
|
|
|
Make evaluation order explicit.
(Do not rely anymore on ocaml evaluation order, which is unspecified.)
|
|
|
|
|
|
|
|
|
|
eager meta substition in w_unify, so as to preserve compatibility
after PMP's move of (setoid) rewrite clauses from metas to
evars (fbbe491cfa).
Hoping it is compatible for non-rewrite uses of the eager meta flag,
and that it is not too costly.
|
|
|
|
|
|
This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
|
|
on vm and #3068 by Nov 2 commit on destruct.
Also fixed test for failure of #3459.
|
|
with evars.
|
|
|
|
|
|
|
|
This is mainly shuffling code around and removing internal
refs that are not needed anymore.
|
|
for residual unifiable evars (otherwise "thin" from logic.ml, erases
the src field) + typo.
|
|
intrusive residual local definitions + more conservative strategy for
which variables are not generalized (point 2 of 4df1ddc6d6bd07073).
|
|
|
|
|
|
Instead of keeping checking that evars are pending, we cache the pending
evars in a proper set computed once and for all.
|
|
|
|
local definitions...
|
|
- It removes some redundancies.
- It fixes failures when destructing a term mentioning goal hypotheses
x1, ..., xn or a term which is a section variable x when this term
is in a type with indices, and the indices also occur in the type of
one of x1, ..., xn, or of x.
- It fixes non-respect of eliminator type when completing pattern possibly
given by a prefix.
- It fixes b2e1d4ea930c which was dealing with the case when the term
was a section variable (it was unfortunately also breaking some
compatibility about which variables variable were generalized in
induction and which variables were automatically cleared because
unselected).
|
|
|
