coq - The formal proof system

Age	Commit message (Expand)	Author
2010-03-06	Fixes in rewrite and a Elimination/Case to Scheme:	msozeau
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-17	Variant !F M for functor application that does not honor the Inline declarations	letouzey
2010-01-07	Include can accept both Module and Module Type	letouzey
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2009-12-27	Fix "Existing Instance" to handle globality information and "Existing	msozeau
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-07	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-18	Module subtyping : allow many <: and module type declaration with <:	letouzey
2009-11-16	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey
2009-11-16	Include Self (Type) Foo: applying a (Type) Functor to the current context	letouzey
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-08-14	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack
2009-08-11	Add support for "Infix ... := constr" instead of just "Infix ... := ref".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-09	Optionally list opaque constants in addition to axions/variables in	msozeau
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-19	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-17	DISCLAIMER	puech
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-10	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau
2008-11-09	Oops... forgot to commit a file related to r11561.	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-09-14	Add user syntax for creating hint databases [Create HintDb foo	msozeau
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau
2008-09-07	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau
2008-08-22	- New auto hints for transparency/opacity control, not bound to	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-07	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau
2008-06-06	Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematical	herbelin
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-22	Strategy commands are now exported	barras