coq - The formal proof system

Age	Commit message (Expand)	Author
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	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-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	Now "Include Self <expr>" handles partially applied functors, cf for example ...	soubiran
2009-11-18	Allow interactive proofs in module types	letouzey
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-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	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-10-09	Fix bug #2162 and a name clashing bug in generalized binders.	msozeau
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-22	Add the option to automatically introduce variables declared before the	msozeau
2009-09-17	Replace call to where_in_path by find_file_in_path in "Locate File"	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-14	Backtrack on the forced discharge of type class variables introduced	msozeau
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-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-05-27	Fix implicit args code so that declarations are added for all	msozeau
2009-05-27	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	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-18	Backporting from v8.2 to trunk:	herbelin
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-17	DISCLAIMER	puech
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	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-23	Minor improvement to commit 11619	herbelin
2008-11-23	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin
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-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-10-03	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau
2008-09-14	Add user syntax for creating hint databases [Create HintDb foo	msozeau