coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7898: Remove camlp4 remains	Emilio Jesus Gallego Arias	2018-07-11
\|\
\| *	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot	2018-07-07
* \|	[vernac] use a record for the contents of the “deprecated” attribute	Vincent Laporte	2018-07-03
* \|	[vernac] use plain strings as attribute names	Vincent Laporte	2018-07-03
* \|	[vernac] Generic syntax for flags/attributes	Vincent Laporte	2018-07-03
* \|	[vernac] Add a “deprecated” attribute	Vincent Laporte	2018-07-03
* \|	[vernac] mk_atts: an atts record with default values	Vincent Laporte	2018-07-03
* \|	[vernac] attribute_of_flags	Vincent Laporte	2018-07-03
\|/
*	Add flag Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
*	Implement uniform parameters in ComInductive	Jasper Hugunin	2018-07-01
*	Make Environ.globals abstract.	Gaëtan Gilbert	2018-06-28
*	Handle mutual record at the vernac level.	Pierre-Marie Pédrot	2018-06-24
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
*	Merge PR #7315: An attempt to clarify error message for Arguments needing "re...	Maxime Dénès	2018-06-04
\|\
* \	Merge PR #7558: [api] Make `vernac/` self-contained.	Maxime Dénès	2018-05-30
\|\ \
* \ \	Merge PR #7521: Fix soundness bug with VM/native and cofixpoints	Pierre-Marie Pédrot	2018-05-28
\|\ \ \
\| * \| \|	Unify pre_env and env	Maxime Dénès	2018-05-28
\| \| * \|	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
\| \| * \|	[tactics] Turn boolean locality hint parameter into a named one.	Emilio Jesus Gallego Arias	2018-05-27
\| \|/ /
* / /	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\|/ /
\| *	An attempt to clarify error message for Arguments needing "rename" flag.	Hugo Herbelin	2018-05-25
\|/
*	[api] Move `Vernacexpr` to parsing.	Emilio Jesus Gallego Arias	2018-05-23
*	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias	2018-05-23
*	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\
* \|	[ide] Remove special option `-ideslave`	Emilio Jesus Gallego Arias	2018-05-21
\| *	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\|/
*	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
*	Merge PR #6935: Separate universe minimization and evar normalization functions	Pierre-Marie Pédrot	2018-04-30
\|\
* \	Merge PR #6958: [lib] Move global options to their proper place.	Maxime Dénès	2018-04-30
\|\ \
* \ \	Merge PR #7152: [api] Remove dependency of library on Vernacexpr.	Pierre-Marie Pédrot	2018-04-23
\|\ \ \
\| \| \| *	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert	2018-04-17
\| \|_\|/ \|/\| \|
* \| \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| * \|	[api] Remove dependency of library on Vernacexpr.	Emilio Jesus Gallego Arias	2018-04-06
\|/ /
* \|	Merge PR #7016: Make parsing independent of the cumulativity flag.	Enrico Tassi	2018-04-05
\|\ \
* \ \	Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.	Enrico Tassi	2018-04-04
\|\ \ \
\| \| \| *	[lib] Move global options to their proper place.	Emilio Jesus Gallego Arias	2018-04-02
\| \|_\|/ \|/\| \|
\| * \|	[stm] Move VernacBacktrack to the toplevel.	Emilio Jesus Gallego Arias	2018-04-01
* \| \|	Remove deprecated commands Arguments Scope and Implicit Arguments	Jasper Hugunin	2018-03-30
\|/ /
\| *	bool option -> (VernacCumulative \| VernacNonCumulative) option	Gaëtan Gilbert	2018-03-22
\| *	Make parsing independent of the cumulativity flag.	Gaëtan Gilbert	2018-03-21
* \|	[vernac] Move `Quit` and `Drop` to the toplevel layer.	Emilio Jesus Gallego Arias	2018-03-11
\|/
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	2018-03-09
*	Export the various option localities in the API.	Pierre-Marie Pédrot	2018-03-09
*	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\ \
* \| \|	[vernac] Warn when using “Require” in a section	Vincent Laporte	2018-03-07
\| * \|	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
\|/ /