coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
*	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias	2018-05-30
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	Adding general support for irrefutable disjunctive patterns.	Hugo Herbelin	2018-02-20
*	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
*	Fix mli-doc issue #6531	Tony Beta Lambda	2018-01-01
*	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	[interp] [ast] Make raw_cases_pattern_expr private.	Emilio Jesus Gallego Arias	2017-05-15
* \|	[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
* \|	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...	Maxime Dénès	2017-04-12
\|\
* \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
* \|	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
\| *	Factorizing/unifying code in dealing with binders.	Hugo Herbelin	2017-03-23
\| *	Improving the API of constrexpr_ops.mli.	Hugo Herbelin	2017-03-23
\|/
*	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
*	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
*	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	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
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot	2012-12-14
*	More equality functions	ppedrot	2012-11-25
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29