coq - The formal proof system

Age	Commit message (Expand)	Author
2011-12-16	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin
2011-10-28	Remove dynamic stuff from constr_expr and glob_constr	glondu
2011-08-30	Quick improvement of some error messages related to module application	herbelin
2011-07-22	Add a syntax entry for fully applied constructor pattern	pboutill
2011-06-12	Rather quick hack to avoid using notations involving "Type" when	herbelin
2011-06-08	Make Notation works with anonymous-level "Type".	herbelin
2011-04-15	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin
2011-02-11	Annotations at functor applications:	letouzey
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-12-04	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-29	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-03-29	Several bug-fixes and improvements of coqdoc	herbelin
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
2009-12-24	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin
2009-12-12	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	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-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	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-01-20	Fixing a bug in 11804 (support for _ in ident entry of notations).	herbelin
2009-01-19	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-10-22	A much better implementation of implicit generalization:	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-07-07	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin
2008-07-04	Fixes in handling of implicit arguments:	msozeau
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-24	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin