coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Using an "as" clause when needed for printing irrefutable patterns.	Hugo Herbelin	2018-02-20
*	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
*	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\
* \|	Fixing #5523 (missing support for complex constructions in recursive notations).	Hugo Herbelin	2017-05-31
* \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
* \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| * \|	Adding a fold_glob_constr_with_binders combinator.	Hugo Herbelin	2017-04-13
\|/ /
\| *	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
\|/
*	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