| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-11-03 | Writing rename_hyps in the new monad. | Pierre-Marie Pédrot | |
| This new implementation now allows for simultaneous replacing of hypotheses, thus fixing bug #2149. | |||
| 2014-11-03 | New bugs revealed fixed: #3408 by (probably) Maxime's commits | Hugo Herbelin | |
| on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459. | |||
| 2014-11-03 | Now that evars can be parsed, protect strongly Check from calling kernel ↵ | Hugo Herbelin | |
| with evars. | |||
| 2014-11-03 | Fixing confused code for interpretations of evar instances. | Hugo Herbelin | |
| 2014-11-03 | vernac_classifier: VernacDeclareTacticDefinition does not alter the parser | Enrico Tassi | |
| 2014-11-03 | Show: do print the goals | Enrico Tassi | |
| 2014-11-03 | STM: code refactoring | Enrico Tassi | |
| This is mainly shuffling code around and removing internal refs that are not needed anymore. | |||
| 2014-11-03 | Subtle swap of lines to preserve VarInstance src field before checking | Hugo Herbelin | |
| for residual unifiable evars (otherwise "thin" from logic.ml, erases the src field) + typo. | |||
| 2014-11-03 | Fix to 844431761 on improving elimination with indices, getting rid of | Hugo Herbelin | |
| intrusive residual local definitions + more conservative strategy for which variables are not generalized (point 2 of 4df1ddc6d6bd07073). | |||
| 2014-11-03 | STM: fix printing of goals when on a tty interface | Enrico Tassi | |
| 2014-11-03 | Fix error reporting id on VtUnknown commands | Enrico Tassi | |
| 2014-11-03 | Fixing inefficiency in typeclass resolution. | Pierre-Marie Pédrot | |
| Instead of keeping checking that evars are pending, we cache the pending evars in a proper set computed once and for all. | |||
| 2014-11-02 | Saving some nf_evars in the code of destruct/induction. | Hugo Herbelin | |
| 2014-11-02 | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin | |
| local definitions... | |||
| 2014-11-02 | Some reorganization of the code for destruct/induction: | Hugo Herbelin | |
| - 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). | |||
| 2014-11-02 | Fixing subterm matched for destruct when it is matched from prefix. | Hugo Herbelin | |
| 2014-11-02 | Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct". | Hugo Herbelin | |
| 2014-11-02 | Plural and singular forms in error messages. | Hugo Herbelin | |
| 2014-11-02 | Cosmetic changes. | Hugo Herbelin | |
| 2014-11-02 | Fixing 1177da327 (reorganization of the test for generic selection of | Hugo Herbelin | |
| occurrences: some uniformisation was not appropriate for "change"). | |||
| 2014-11-02 | Fixing file destruct.v. | Hugo Herbelin | |
| 2014-11-01 | Document [Info] command. | Arnaud Spiwack | |
| 2014-11-01 | Info: the warning message of the defunct [info] tactic now points to the ↵ | Arnaud Spiwack | |
| [Info] command. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |