aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Relax uniform inheritance conditionGravatar gareuselesinge2012-04-05
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
* Force Check (which, from 8.4beta, accepts unresolved evars) to howeverGravatar herbelin2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Fix merge and add missing file.Gravatar msozeau2012-03-14
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Integrated obligations/eterm and program well-founded fixpoint building to to...Gravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Bug 2703: send stdout dump to coqide when an error occurs.Gravatar pboutill2012-02-29
* Arguments supports extra notation scopesGravatar gareuselesinge2012-02-14
* More information returned by coqtop about its internal state. Hopefully we'll...Gravatar ppedrot2012-02-02
* Fail: discard the effects of a successful command (fix #2682)Gravatar letouzey2012-01-26
* Add support for plugin initialization functionGravatar gareuselesinge2012-01-26
* Check for unresolved evars in textual order of the params and fields declarat...Gravatar msozeau2012-01-25
* Fix typeclass resolution error message which included goal evars (bug #2620).Gravatar msozeau2012-01-23
* Removed a seemingly unused argument in Require of modules, introduced 10 year...Gravatar ppedrot2012-01-23
* Bug 739: forbid dumpglob while using Coqtop in interactive modeGravatar pboutill2012-01-23
* Added new command "Set Parsing Explicit" for deactivating parsing (andGravatar herbelin2012-01-20
* sequel of previous commitGravatar letouzey2011-12-21
* Pure interfaces shouldn't be mentionned in .mllibGravatar letouzey2011-12-21
* Arguments: check rename even if no implicit is specifiedGravatar gareuselesinge2011-12-19
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
* Deactivated automatic inference of _case schemes, as it was in 8.3Gravatar herbelin2011-12-17
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
* Moving bullets (-, +, *) into stand-alone commands instead of beingGravatar courtieu2011-12-16
* Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...Gravatar ppedrot2011-12-15
* Proof using ...Gravatar gareuselesinge2011-12-12
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
* More type safety in query GADT (again).Gravatar ppedrot2011-11-30
* Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...Gravatar ppedrot2011-11-30
* Fixed a warning about unused variable introduced in r14731Gravatar ppedrot2011-11-29
* Added an API call to retrieve and change the option stateGravatar ppedrot2011-11-25
* Separated the toplevel interface into a purely declarative module with associ...Gravatar ppedrot2011-11-25
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Moving XML handling to lib directoryGravatar ppedrot2011-11-24
* Correct direction for definitional typeclassesGravatar msozeau2011-11-24
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
* New Arguments vernacularGravatar gareuselesinge2011-11-21