coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	"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
*	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
*	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
*	A pass on warning printings. Made systematic the use of msg_warning so	herbelin	2011-12-17
*	Fixing association of wrong "as"-pattern name when expanding	herbelin	2011-11-16
*	Remove dynamic stuff from constr_expr and glob_constr	glondu	2011-10-28
*	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
*	A correct error message for an unknown field in a record definition	pboutill	2011-07-15
*	Partial fix for accepting bound variables with same name as implicit	herbelin	2011-05-26
*	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin	2011-04-25
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	local variables can have implicits locally	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	internalize now use a record for its env	pboutill	2011-02-10
*	More comments and less doublons in some mli	pboutill	2011-02-10
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
*	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
*	Add information of localisation when an error involving an "implicit	herbelin	2010-11-07
*	Fixing a regression wrt 8.2 when using an "ident" several times in a notation	herbelin	2010-11-04
*	Cleaning the use of parentheses around evd and evdref (cosmetic commit).	herbelin	2010-10-31
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	Bugfix: A notation for a constructor where some arguments are _	pboutill	2010-09-10
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Constrintern: Moved section about binders before section about notation	herbelin	2010-07-22
*	Switch to American spelling for "internalise" and "internalisation"	herbelin	2010-07-22
*	Fixing bug 2295 (omission of option "as" in return clause of "match" was not	herbelin	2010-06-13
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau	2010-06-09
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Partially fixed bug #2231 (an inductive parameter name was internally	herbelin	2010-04-10
*	Improving compatibility between 8.2 and 8.3	herbelin	2010-04-05
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29