aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2012-04-18Corrects a (very) longstanding bug of tactics. As is were, tactic expectingaspiwack
2012-04-17Bug 2733 : { } implicits and Fixpointspboutill
2012-04-13Better error message when defining recursive records with Record oraspiwack
2012-04-12Remove print call that do not use the pp mechanismpboutill
2012-04-12lib directory is cut in 2 cma.pboutill
2012-04-05Relax uniform inheritance conditiongareuselesinge
2012-03-30Added a command "Unfocused" which returns an error when the proof isaspiwack
2012-03-30Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclletouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-23Remove undocumented command "Delete foo"letouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-20Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicherbelin
2012-03-20Force Check (which, from 8.4beta, accepts unresolved evars) to howeverherbelin
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-14Fix merge and add missing file.msozeau
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2012-03-14Everything compiles again.msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-02Noise for nothingpboutill
2012-02-29Bug 2703: send stdout dump to coqide when an error occurs.pboutill
2012-02-14Arguments supports extra notation scopesgareuselesinge
2012-02-02More information returned by coqtop about its internal state. Hopefully we'll...ppedrot
2012-01-26Fail: discard the effects of a successful command (fix #2682)letouzey
2012-01-26Add support for plugin initialization functiongareuselesinge
2012-01-25Check for unresolved evars in textual order of the params and fields declarat...msozeau
2012-01-23Fix typeclass resolution error message which included goal evars (bug #2620).msozeau
2012-01-23Removed a seemingly unused argument in Require of modules, introduced 10 year...ppedrot
2012-01-23Bug 739: forbid dumpglob while using Coqtop in interactive modepboutill
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
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