coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Program: avoid staying in program mode after a failed Program command	letouzey	2012-04-26
*	correct abort in Function when a proof of inversion fails	letouzey	2012-04-23
*	Corrects a (very) longstanding bug of tactics. As is were, tactic expecting	aspiwack	2012-04-18
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Added a command "Unfocused" which returns an error when the proof is	aspiwack	2012-03-30
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey	2012-03-23
*	Remove undocumented command "Delete foo"	letouzey	2012-03-23
*	Remove old proof-managment commands Suspend/Resume	letouzey	2012-03-23
*	Force Check (which, from 8.4beta, accepts unresolved evars) to however	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Removed a seemingly unused argument in Require of modules, introduced 10 year...	ppedrot	2012-01-23
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	Arguments: check rename even if no implicit is specified	gareuselesinge	2011-12-19
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
*	Proof using ...	gareuselesinge	2011-12-12
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Correct direction for definitional typeclasses	msozeau	2011-11-24
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	Adding the type infrastructure to handle properly API management of options	ppedrot	2011-11-18
*	Restore backward compatibility. ":>" declares subinstances in Class declarati...	msozeau	2011-11-18
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey	2011-10-25
*	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey	2011-09-15
*	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack	2011-09-12
*	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey	2011-09-05
*	Remove code concerning the obsolete Set/Unset Undo	letouzey	2011-09-05
*	Misc improvements concerning "Show Match" and its coqide equivalent	letouzey	2011-08-18
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
*	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack	2011-05-13
*	Print Module (Type) M now tries to print more details	letouzey	2011-05-11
*	Fixed a bug causing inconsistent states during proof editting.	aspiwack	2011-04-29
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13
*	Fixed "Eval ... in t" when t has still metavariables.	herbelin	2011-04-08
*	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey	2011-04-06
*	Goptions: repair Unset for int options	letouzey	2011-03-17
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Annotations at functor applications:	letouzey	2011-02-11
*	Started to fix the declarative proof mode (C-zar).	aspiwack	2011-02-10
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28