aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Restore backward compatibility. ":>" declares subinstances in Class declarati...Gravatar msozeau2011-11-18
* Fix for subclasses implementation, allowing to register generalized classes s...Gravatar msozeau2011-11-18
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Merge fix for bug #2604.Gravatar msozeau2011-11-17
* Fix bug #2604, wrong error from setoid_rewrite. The rewrite is impossible due...Gravatar msozeau2011-11-17
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Was missing a potential application of subtypingGravatar msozeau2011-11-17
* Adding postprocessing to remove "commutative cuts" expansions inGravatar herbelin2011-11-16
* Changed the way find_dependencies_signature is working so that itGravatar herbelin2011-11-16
* De Bruijn indices bug in pattern matching compilation in the presenceGravatar herbelin2011-11-16
* Old generalization bug in pattern-matching: names were considered theGravatar herbelin2011-11-16
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Old typing bug in pattern-matching compilation (apparently w/oGravatar herbelin2011-11-16
* Specialization of tomatch in pattern-matching compilation was done tooGravatar herbelin2011-11-16
* A bit of documentation around cases.ml + ML modules uselessly openGravatar herbelin2011-11-16
* Completed list of theories targetsGravatar herbelin2011-11-16
* Suppression fichier Case8.v redondantGravatar herbelin2011-11-16
* Fixing beautification of "thm_token" (missing space) + improvements.Gravatar herbelin2011-11-16
* Fixing association of wrong "as"-pattern name when expandingGravatar herbelin2011-11-16
* Fixing dependencies lifting bug in pattern-matching compilationGravatar herbelin2011-11-16
* Bug 2637: patches to make slightly easier to write programs that use coq code...Gravatar pboutill2011-11-14
* Bug 2636 - Move string_of_ppcmds to PpGravatar pboutill2011-11-14
* Fixed ocamlbuild compilation (Tom Prince)Gravatar ppedrot2011-11-09
* Refined second_order_matching so that a constraint on whichGravatar herbelin2011-11-08
* optimization: memoization for is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
* Fixed xml-light handling of whitespace not compliant with XML standard: it st...Gravatar ppedrot2011-11-07
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06
* Fixing tactic remember not correctly checking preservation of typingGravatar herbelin2011-11-06
* Also sprach CoqIDE (in XML)Gravatar ppedrot2011-11-06
* Fixed nasty bug when empty PCData, confusion no string vs. empty stringGravatar ppedrot2011-11-06
* More XML marshalling functionsGravatar ppedrot2011-11-06
* Added XML dependencies into MakefileGravatar ppedrot2011-11-06
* Partialliy added XML marshalling to ide_intfGravatar ppedrot2011-11-06
* Added XML manipulation tools to compilation chainGravatar ppedrot2011-11-06
* Added XML manipulation basics (modified from xml-light)Gravatar ppedrot2011-11-06
* Added missing printing debug functions in IDE interfaceGravatar ppedrot2011-11-05
* Auto: removal of ?use_core_db obsolete now that we have nocoreGravatar letouzey2011-11-04
* Cleaning a little bit the files talking about descriptions: avoidingGravatar herbelin2011-11-03
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).Gravatar herbelin2011-10-29
* Fixed broken globalization of identifiers containing utf8 lettersGravatar herbelin2011-10-29
* Added checksums to glob files and warned about possibly missingGravatar herbelin2011-10-29
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Remove avoidable use of GDynamicGravatar glondu2011-10-27
* Deactivating second-order pattern-matching in evarconv for 8.4.Gravatar herbelin2011-10-26
* Fix configuration box bug in recursive callGravatar pboutill2011-10-26
* Coq_makefile handles .mlpack filesGravatar pboutill2011-10-26