coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing the "capture" check newly introduced in r15122 when	herbelin	2012-04-07
*	Unifying the different procedures for interning binders.	herbelin	2012-04-06
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	Fixing deactivation of scope at printing time in the body of a	herbelin	2012-03-26
*	Fixing bug #2724 (using notations with binders in cases patterns	herbelin	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin	2012-03-20
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Second step of integration of Program:	msozeau	2012-03-14
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
*	"Let in" in pattern hell, one more iteration	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	Fix compilation of Constrintern...	pboutill	2012-02-29
*	RefMan update about match syntax.	pboutill	2012-02-29
*	In the syntax of pattern matching, the arguments of the inductive in the "in"	pboutill	2012-02-29
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin	2012-02-01
*	Printing bugs with match patterns:	herbelin	2012-01-27
*	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin	2012-01-20
*	Added new command "Set Parsing Explicit" for deactivating parsing (and	herbelin	2012-01-20
*	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
*	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin	2012-01-05
*	Fixing Arguments Scope bug when too many scopes are given (bug #2667).	herbelin	2012-01-04
*	Fixing bug #2634 (unscoped notations were disturbing the	herbelin	2011-12-18
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	New Arguments vernacular	gareuselesinge	2011-11-21
*	Fixing association of wrong "as"-pattern name when expanding	herbelin	2011-11-16
*	Allow "\|_=>_" in "match" in patterns, no more forced enumeration of constructors	letouzey	2011-11-07
*	Add type annotations around all calls to Libobject.declare_object	letouzey	2011-11-02
*	Fixed broken globalization of identifiers containing utf8 letters	herbelin	2011-10-29
*	Added checksums to glob files and warned about possibly missing	herbelin	2011-10-29
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	Fixing failing printer when the type of a binder name with implicit	herbelin	2011-10-24
*	Quick improvement of some error messages related to module application	herbelin	2011-08-30
*	Fixing printing bug with last trailing non-maximally implicit	herbelin	2011-08-10
*	Partial revert of r14292	pboutill	2011-07-26
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	Internalization of pattern carries a full intern_env	pboutill	2011-07-22
*	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin	2011-07-16
*	This option disables the use of the '{\| field := ... \|}' notation	herbelin	2011-07-16
*	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin	2011-07-16
*	A correct error message for an unknown field in a record definition	pboutill	2011-07-15
*	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