coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Use dashed lines for equivalence edges in dot output of universes	glondu	2011-01-11
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Add information of localisation when an error involving an "implicit	herbelin	2010-11-07
*	In Univ, unify order_request and constraint_type	glondu	2010-11-03
*	Output universe graph in DOT language if output file ends in .dot or .gv	glondu	2010-11-02
*	More generic Univ.dump_universes	glondu	2010-11-02
*	Add tolerance for existential variables in Check.	herbelin	2010-10-31
*	Remove Explain* vernacs	glondu	2010-10-06
*	Remove VernacGo	glondu	2010-10-06
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Making display of various informations about constants more modular:	herbelin	2010-10-03
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28