| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-11-07 | Print [rename] tactic properly in info trace. | Arnaud Spiwack | |
| Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad). | |||
| 2014-11-06 | Consequence of changing the definition of Nat.shiftl and Nat.shiftr. | Hugo Herbelin | |
| 2014-11-06 | Restoring clear_flag (thanks a lot to jonikelee to notice it). | Hugo Herbelin | |
| 2014-11-06 | Optimizing when to clear generalized hypotheses in destruct. | Hugo Herbelin | |
| Removing blocking of generalization on destructed hypothesis introduced on Nov 2. It was a bad idea as shown by bug #3790 on eliminating v:Vector n, keeping an equality. | |||
| 2014-11-06 | Dependency bug in using eqn for destruct. | Hugo Herbelin | |
| 2014-11-06 | Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels. | Hugo Herbelin | |
| 2014-11-06 | Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels) | Hugo Herbelin | |
| by hopefully computing the right position where to reinit an empty level. Also removing obsolete comment. | |||
| 2014-11-06 | Removing "destruct" test not yet working. | Hugo Herbelin | |
| 2014-11-06 | Fixing compilation (name of module Richprinter) I partially feel | Hugo Herbelin | |
| responsible about. | |||
| 2014-11-05 | lib/RichPp: Rename into Richpp. | Yann Régis-Gianas | |
| printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |