aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* coqrc in the right XDG_CONFIG_HOME/coq folderGravatar pboutill2011-11-20
* coqide-gtk2rc not dottedGravatar pboutill2011-11-20
* CoqIdE configuration file won't pollute your home anymoreGravatar pboutill2011-11-20
* Teach coq_makefile how to install into XDG_DATA_HOME.Gravatar pboutill2011-11-20
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
* coq_makefile: Don't install with +x.Gravatar pboutill2011-11-20
* coq_makefile: Add Makefile variables specifying installGravatar pboutill2011-11-20
* Adding the type infrastructure to handle properly API management of optionsGravatar ppedrot2011-11-18
* Fix parsing of :>> and backtrack correctly on the cache of hints for local co...Gravatar msozeau2011-11-18
* Return of the tactic hints features in CoqIDE.Gravatar ppedrot2011-11-18
* Added hint support in the API. You can now query a goal to see the tactics th...Gravatar ppedrot2011-11-18
* Toplevel loop is a bit more robust: it catches bad API queries.Gravatar ppedrot2011-11-18
* Making status info better in CoqIDE: path and name of current lemmaGravatar ppedrot2011-11-18
* Now Coqtop has a richer way to answer a query about its pending goals. Answer...Gravatar ppedrot2011-11-18
* Added a printing function to handle single evarsGravatar ppedrot2011-11-18
* Replaced goal api call with a proper structure. This disables menu hints in C...Gravatar ppedrot2011-11-18
* Coqide -debug only printed Coqtop information.Gravatar pboutill2011-11-18
* 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