coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correct some spelling errorsmaster	Benjamin Barenblat	2018-07-22
*	Merge PR #7746: Many small cleanups removing unused arguments and functions	Pierre-Marie Pédrot	2018-07-05
\|\
\| *	Coq_omega: remove unused Goal.enters	Gaëtan Gilbert	2018-07-03
\| *	Remove unused function Coq_omega.timing.	Gaëtan Gilbert	2018-07-03
* \|	Moving various ml4 files to mlg.	Pierre-Marie Pédrot	2018-07-02
\|/
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès	2018-02-21
\|\
* \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| *	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
\|/
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Using is_conv rather than eq_constr to find `nat` or `Z` in omega.	Hugo Herbelin	2017-11-23
*	Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...	Pierre Letouzey	2017-10-05
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond	2017-09-12
*	[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
*	Merge PR#673: Two fixes about zify (bugs #5336 and #5439)	Maxime Dénès	2017-06-14
\|\
* \|	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot	2017-06-13
* \|	Explicit the unsafe flag of all calls to Refine.refine.	Pierre-Marie Pédrot	2017-06-13
* \|	Merge PR#718: API cleanup: aliases	Maxime Dénès	2017-06-12
\|\ \
\| \| *	zify: force reduction of (Z.max 0 0) and similar (fix #5439)	Pierre Letouzey	2017-06-12
\| \| *	zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)	Pierre Letouzey	2017-06-12
\| \|/ \|/\|
* \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| *	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\ \ \| \|/ \|/\|
* \|	Put all plugins behind an "API".	Matej Kosik	2017-06-07
* \|	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
* \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| *	Fix bug #5019 (looping zify on dependent types)	Jason Gross	2017-06-01
\| *	Omega: use "simpl" only on coefficents, not on atoms (fix #4132)	Pierre Letouzey	2017-05-29
* \|	Cleanup: removal of constr_of_global.	Matthieu Sozeau	2017-05-29
* \|	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\ \
\| * \|	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \| \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
\|/ /
* \|	Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...	Maxime Dénès	2017-05-26
\|\ \
* \| \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| * \|	refl_omega: some code refactoring	Pierre Letouzey	2017-05-22
\| * \|	ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT	Pierre Letouzey	2017-05-22
\|/ /
* \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
* \|	Porting omega to the new tactic API.	Pierre-Marie Pédrot	2017-04-24
* \|	Removing trivial compatibility layer in omega.	Pierre-Marie Pédrot	2017-04-24
* \|	Fix an unhandled exception in Omega.	Pierre-Marie Pédrot	2017-04-07
* \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
* \|	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
* \| \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14