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-08	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey
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-15	Document Generalizable Variables, and change syntax to	msozeau
2009-11-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-06	Misc fixes.	msozeau
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-28	Module type expressions of the form (Fsig X) with Definition foo := bar are n...	soubiran
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-10-25	Improved the treatment of Local/Global options (noneffective Local on	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-14	- Addition of "Reserved Infix" continued.	herbelin
2009-09-13	- Inductive types in the "using" option of auto/eauto/firstorder are	herbelin
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-09-02	Postpone checking of Local/Global to allow grammar extensions to use it	msozeau
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-07-15	- Granted wish #2138 (support for local binders in syntax of Record fields).	herbelin
2009-06-15	Allow anonymous instances again, with syntax [Instance: T] where T	msozeau
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey
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-02-03	Do not reserve the keyword "Infer".	puech
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	Last changes in type class syntax:	msozeau
2009-01-17	DISCLAIMER	puech
2009-01-14	Fixing/improving management of uniform prefix Local and Global	herbelin
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
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-10	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	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-20	Renommage "Global Instance" en "Instance Global" pour uniformisation	herbelin