coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
*	Partial fix to #4592 (notation requiring alpha-conversion for printing).	Hugo Herbelin	2016-07-17
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
*	Fixing equality of notation_constrs. Fixes bug #4136.	Pierre-Marie Pédrot	2015-03-24
*	Update headers.	Maxime Dénès	2015-01-12
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	Glob-ops: a name-mapping operation for pattern-matching binders.	Arnaud Spiwack	2014-11-19
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Adding an equality function over glob_constr	Pierre-Marie Pédrot	2014-03-02
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Added a constr_pattern_eq	ppedrot	2012-11-23
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29