coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7558: [api] Make `vernac/` self-contained.	Maxime Dénès	2018-05-30
\|\
\| *	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
* \|	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\|/
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
*	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
*	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
*	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	[printing] Remove duplicated printing function.	Emilio Jesus Gallego Arias	2017-06-01
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\
* \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\| \|\ \| \|/ \|/\|
* \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
\| *	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\| *	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
*	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-06-16
*	Fixing printing of Function.	Hugo Herbelin	2016-06-16
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	More toplevel value representation sharing.	Pierre-Marie Pédrot	2016-05-04
*	Revert "Fixing printing of Function."	Hugo Herbelin	2016-04-27
*	Revert "Fixing a mispelling coma -> comma."	Hugo Herbelin	2016-04-27
*	Fixing a mispelling coma -> comma.	Hugo Herbelin	2016-04-27
*	Fixing printing of Function.	Hugo Herbelin	2016-04-27
*	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
*	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20