coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Notations are back in the "in" clause of pattern matching.	pboutill	2012-05-15
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Fixing bug #2724 (using notations with binders in cases patterns	herbelin	2012-03-20
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Notations with binders: Accepting using notations for functional terms	herbelin	2012-01-20
*	Boolean Option Patterns Compatibility	pboutill	2012-01-19
*	Parameters in pattern first step.	pboutill	2012-01-16
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	Rather quick hack to avoid using notations involving "Type" when	herbelin	2011-06-12
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	Annotations at functor applications:	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).	herbelin	2010-12-04
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Variant !F M for functor application that does not honor the Inline declarations	letouzey	2010-01-17
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	Opened the possibility to type Ltac patterns but it is not fully functional yet	herbelin	2009-12-24
*	Fixed incorrect computation of possible guard in presence of `{ ... } contexts.	herbelin	2009-12-12
*	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey	2009-12-07
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey	2009-11-16
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Fixing a bug in 11804 (support for _ in ident entry of notations).	herbelin	2009-01-20
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19