coq - The formal proof system

Age	Commit message (Expand)	Author
2011-12-19	Arguments: check rename even if no implicit is specified	gareuselesinge
2011-12-17	Command Arguments: standardizing format of error messages and American spelling.	herbelin
2011-12-16	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu
2011-12-12	Proof using ...	gareuselesinge
2011-12-06	Minor fixes to Arguments	gareuselesinge
2011-11-24	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-21	Renamig support added to "Arguments"	gareuselesinge
2011-11-21	New Arguments vernacular	gareuselesinge
2011-11-18	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-17	Merge subinstances branch by me and Tom Prince.	msozeau
2011-10-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2011-09-15	Re-allowing assumptions during proofs seems safe now (fix #2411)	letouzey
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-09-05	Lib.node: merge OpenedModtype and OpenedModule, same for Closed...	letouzey
2011-09-05	Remove code concerning the obsolete Set/Unset Undo	letouzey
2011-08-18	Misc improvements concerning "Show Match" and its coqide equivalent	letouzey
2011-07-16	This option disables the use of the '{\| field := ... \|}' notation	herbelin
2011-05-13	New option [Set Bullet Behavior] allows to select the behaviour of bullets.	aspiwack
2011-05-11	Print Module (Type) M now tries to print more details	letouzey
2011-04-29	Fixed a bug causing inconsistent states during proof editting.	aspiwack
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-08	Fixed "Eval ... in t" when t has still metavariables.	herbelin
2011-04-06	Add 'Existing Instances' declaration to declare multiple instances at once.	letouzey
2011-03-17	Goptions: repair Unset for int options	letouzey
2011-03-05	Added a table for using reserved names for binding names to types	herbelin
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2011-02-11	Annotations at functor applications:	letouzey
2011-02-10	Started to fix the declarative proof mode (C-zar).	aspiwack
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2011-01-11	Add "Print Sorted Universes"	glondu
2011-01-11	Use dashed lines for equivalence edges in dot output of universes	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-11-07	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-03	In Univ, unify order_request and constraint_type	glondu
2010-11-02	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-10-31	Add tolerance for existential variables in Check.	herbelin
2010-10-06	Remove Explain* vernacs	glondu
2010-10-06	Remove VernacGo	glondu
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-10-03	Making display of various informations about constants more modular:	herbelin
2010-09-28	Fix function applications without labels (OCaml warning 6)	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-18	Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too	herbelin
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu