coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Partial fix for accepting bound variables with same name as implicit	herbelin	2011-05-26
*	Fixing discriminate for identity.	herbelin	2011-05-26
*	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey	2011-05-05
*	Fixing and completing interpretation of let's in notations for iterated binders.	herbelin	2011-04-25
*	Yet another bug in printing fix with let-in binders	herbelin	2011-04-24
*	Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".	herbelin	2011-04-15
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Fixing multiple printing bugs with "Notation f x := ..."	herbelin	2011-04-08
*	Did that adding a rule for printing applications as "f(x)" works.	herbelin	2011-03-31
*	Added a table for using reserved names for binding names to types	herbelin	2011-03-05
*	Moving printing of module typing errors upwards to himsg.ml so as to	herbelin	2011-03-05
*	fix last commit about modules (subst_cl_typ may raise Not_found)	letouzey	2011-02-12
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	Annotations at functor applications:	letouzey	2011-02-11
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
*	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
*	Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"	letouzey	2011-01-31
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Rename mkR* smart constructors (mostly in funind)	glondu	2010-12-25
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Fix diagram in genarg.mli	glondu	2010-12-23
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23