aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* /home/pirbo/.coqrc* are read againGravatar pboutill2011-11-21
* -user option removalGravatar pboutill2011-11-21
* coqrc in the right XDG_CONFIG_HOME/coq folderGravatar pboutill2011-11-20
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
* Adding the type infrastructure to handle properly API management of optionsGravatar 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
* Replaced goal api call with a proper structure. This disables menu hints in C...Gravatar ppedrot2011-11-18
* Restore backward compatibility. ":>" declares subinstances in Class declarati...Gravatar msozeau2011-11-18
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* 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 xml-light handling of whitespace not compliant with XML standard: it st...Gravatar ppedrot2011-11-07
* 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
* 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
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* 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
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Scheme names: Use unprobable names + ensure names do not hide existing namesGravatar herbelin2011-10-08
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
* Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).Gravatar herbelin2011-10-05
* Fixing critical part of bug #2504. Not all inductive types in Type areGravatar herbelin2011-10-01
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
* Re-allowing assumptions during proofs seems safe now (fix #2411)Gravatar letouzey2011-09-15
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Coqide: new backtracking code, based on the Backtrack commandGravatar letouzey2011-09-05
* Ide_intf: slight reorganisation of the IDE apiGravatar letouzey2011-09-05
* Lib.node: merge OpenedModtype and OpenedModule, same for Closed...Gravatar letouzey2011-09-05
* Remove code concerning the obsolete Set/Unset UndoGravatar letouzey2011-09-05
* Quick improvement of some error messages related to module applicationGravatar herbelin2011-08-30
* Clarifying that only identifiers are advertised to be turned into keywordsGravatar herbelin2011-08-23
* Misc improvements concerning "Show Match" and its coqide equivalentGravatar letouzey2011-08-18
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* Improving error message about coinductive guard (old "cases" is now "match")Gravatar herbelin2011-08-10
* Partly revert commit r14389 about relaxing the condition for being a keywordGravatar herbelin2011-08-10
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...Gravatar aspiwack2011-08-09
* Be a bit less aggressive in declaring idents as keywords in notationsGravatar herbelin2011-08-08
* Fix nf_evars_undefined use in pr_constraintsGravatar msozeau2011-08-03
* Class: generic equality on constr replaced by destructorsGravatar puech2011-07-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 01:52:52 +0000