| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-05 | lib/richPp: Fix a bug related to the compatibility with ocaml 3.12 | Yann Régis-Gianas | |
| - The previous version of this module was using a feature of the Format module of ocaml 4.01. - Add comments. | |||
| 2014-11-05 | printing/Ppvernac: Fix missing keyword tagging on theorem introducers. | Yann Régis-Gianas | |
| 2014-11-05 | printing/Ppvernac: Fix missing keyword tagging on definition introducers. | Yann Régis-Gianas | |
| 2014-11-05 | printing/Ppvernac: Cosmetics. | Yann Régis-Gianas | |
| 2014-11-05 | Writing the raw introduction tactic in the new monad. | Pierre-Marie Pédrot | |
| 2014-11-04 | ide/Xmlprotocol: Cosmetics. | Yann Régis-Gianas | |
| 2014-11-04 | lib/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/richPp: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | printing/Ppannotation: New annotation for tactic syntactic objects. | Regis-Gianas | |
| printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services. | |||
| 2014-11-04 | printing/Pptactic.Make: New. | Regis-Gianas | |
| - Functorize with respect to the pretty-printer for constr. - Include the application of Make to Ppconstr at toplevel in order to preserve previous behavior. | |||
| 2014-11-04 | printing/Pptacticsig: New signature for tactic pretty-printers. | Regis-Gianas | |
| printing/Pptactic: Use it. | |||
| 2014-11-04 | lib/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | Rebase artefact. | Regis-Gianas | |
| 2014-11-04 | lib/Pp.tag: New. | Regis-Gianas | |
| A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | printing/Ppannotation: Introduce a new annotation for keywords. | Regis-Gianas | |
| printing/{Ppconstr, Ppvernac}: Use it. | |||
| 2014-11-04 | printing/richPrinter: Fix incorrect signatures. | Regis-Gianas | |
| 2014-11-04 | ide/Ide_slave.annotate: Implement annotate. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_parser.parse: Publish and document new interface. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_printer.pcdata_to_string: Publish. | Regis-Gianas | |
| 2014-11-04 | printing/RichPrinter: New API for rich pretty-printing. | Regis-Gianas | |
| printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping. | |||
| 2014-11-04 | lib/Pp.rewrite: New. | Regis-Gianas | |
| Allow strings of a pretty-print to be rewritten just before the actual output. | |||
| 2014-11-04 | lib/Xml_printer: Handle non-breakable spaces. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_parser.parse: Make canonicalization optional. (By default, it is ↵ | Regis-Gianas | |
| applied, to preserve previous behaviors. | |||
| 2014-11-04 | lib/Xml_parser: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | lib/Xml_parser: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | Xml_lexer: Handle non-breakable spaces. | Regis-Gianas | |
| 2014-11-04 | ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between ↵ | Regis-Gianas | |
| internal and external datatypes. | |||
| 2014-11-04 | ide/wg_ProofView: Do not refer to the {Proof} internal module, use ↵ | Regis-Gianas | |
| {Interface} instead. | |||
| 2014-11-04 | ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate". | Regis-Gianas | |
| - 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.) | |||
| 2014-11-04 | Ppvernac: Publish new rich pretty-printer. | Regis-Gianas | |
| Ppconstr: Fix a typo in comments. | |||
| 2014-11-04 | Ppannotation.t: New constructor AVernac. | Regis-Gianas | |
| Ppvernac.RichPp: New rich pretty-printer. | |||
| 2014-11-04 | Ppvernacsig: New. | Regis-Gianas | |
| - Define the signature for a pretty-printer of vernacular commands. Ppvernac: Use it. | |||
| 2014-11-04 | Ppvernac.Make: New | Regis-Gianas | |
| - Ppvernac is now functorized with respect to a Ppconstr printer. - Preserve previous behavior by instantiating this functor with Ppconstr. | |||
| 2014-11-04 | Ppvernac: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | Ppannotation: New. | Regis-Gianas | |
| 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. | |||
| 2014-11-04 | RichPp: New module. | Regis-Gianas | |
| 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. | |||
| 2014-11-04 | Xml_datatype.gxml: New type for semi-structured documents. | Regis-Gianas | |
| Xml_parser, Xml_printer: Use it. | |||
| 2014-11-04 | lib/Pp: Publish combinators for tags opening and closing. | Regis-Gianas | |
| 2014-11-04 | printing/Ppconstr.Make: | Regis-Gianas | |
| - 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. | |||
| 2014-11-04 | lib/Pp.ppcmd_token: | Regis-Gianas | |
| 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. | |||
| 2014-11-04 | lib/Pp: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | printing/Ppconstr.print_hunks: | Regis-Gianas | |
| Make evaluation order explicit. (Do not rely anymore on ocaml evaluation order, which is unspecified.) | |||
| 2014-11-04 | printing/Ppconstr: Cosmetics. | Regis-Gianas | |
| 2014-11-04 | Removing the old rename tactic. | Pierre-Marie Pédrot | |
| 2014-11-04 | Fixing careless name confusion in CHANGES. | Pierre-Marie Pédrot | |
| 2014-11-04 | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot | |
| 2014-11-04 | Experimentally applying eager evar substitution at the same time as | Hugo Herbelin | |
| 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. | |||
| 2014-11-04 | test suite: some reproduction cases for recently-reported bugs. | Xavier Clerc | |
| 2014-11-04 | Test for bug #2149. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |