aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2011-12-21sequel of previous commitletouzey
2011-12-21Pure interfaces shouldn't be mentionned in .mllibletouzey
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
2011-12-17Deactivated automatic inference of _case schemes, as it was in 8.3herbelin
2011-12-17A pass on warning printings. Made systematic the use of msg_warning soherbelin
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...ppedrot
2011-12-12Proof using ...gareuselesinge
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-11-30More type safety in query GADT (again).ppedrot
2011-11-30Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...ppedrot
2011-11-29Fixed a warning about unused variable introduced in r14731ppedrot
2011-11-25Added an API call to retrieve and change the option stateppedrot
2011-11-25Separated the toplevel interface into a purely declarative module with associ...ppedrot
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-24Moving XML handling to lib directoryppedrot
2011-11-24Correct direction for definitional typeclassesmsozeau
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-21/home/pirbo/.coqrc* are read againpboutill
2011-11-21-user option removalpboutill
2011-11-20coqrc in the right XDG_CONFIG_HOME/coq folderpboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-11-18Adding the type infrastructure to handle properly API management of optionsppedrot
2011-11-18Added hint support in the API. You can now query a goal to see the tactics th...ppedrot
2011-11-18Toplevel loop is a bit more robust: it catches bad API queries.ppedrot
2011-11-18Making status info better in CoqIDE: path and name of current lemmappedrot
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. Answer...ppedrot
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in C...ppedrot
2011-11-18Restore backward compatibility. ":>" declares subinstances in Class declarati...msozeau
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-14Bug 2637: patches to make slightly easier to write programs that use coq code...pboutill
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-11-07Fixed xml-light handling of whitespace not compliant with XML standard: it st...ppedrot
2011-11-06Also sprach CoqIDE (in XML)ppedrot
2011-11-06Fixed nasty bug when empty PCData, confusion no string vs. empty stringppedrot
2011-11-06More XML marshalling functionsppedrot
2011-11-06Partialliy added XML marshalling to ide_intfppedrot
2011-11-06Added XML manipulation tools to compilation chainppedrot
2011-11-06Added XML manipulation basics (modified from xml-light)ppedrot
2011-11-05Added missing printing debug functions in IDE interfaceppedrot
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-29Added checksums to glob files and warned about possibly missingherbelin
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin