coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correct some spelling errorsmaster	Benjamin Barenblat	2018-07-22
*	Moving various ml4 files to mlg.	Pierre-Marie Pédrot	2018-07-02
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	romega: get rid of EConstr.Unsafe	Pierre Letouzey	2018-03-06
*	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\
* \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\|/
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
*	Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion	Maxime Dénès	2017-11-24
\|\
\| *	Recognizing Z in romega up to conversion.	Hugo Herbelin	2017-11-23
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\|/
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	romega: takes advantage of context variables with body	Pierre Letouzey	2017-10-05
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	romega: avoid potential slowdown when changing concl by reified version	Pierre Letouzey	2017-06-16
*	Merge PR#718: API cleanup: aliases	Maxime Dénès	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
\|/
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	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
* \|	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	ROmega: division-aware ReflOmegaCore, allowing trace without terms	Pierre Letouzey	2017-05-24
*	refl_omega: some code refactoring	Pierre Letouzey	2017-05-22
*	refl_omega.v: explicitely identify atom indexes and omega vars	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: misc cleanup, <? instead of bgt, etc	Pierre Letouzey	2017-05-22
*	ROmega : O_STATE turned into a O_SUM	Pierre Letouzey	2017-05-22
*	ROmega: less contructors in the final omega trace	Pierre Letouzey	2017-05-22
*	ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple)	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: comment, reorganize, permut some constructors, etc	Pierre Letouzey	2017-05-22
*	romega: add a tactic named unsafe_romega (for debugging, or bold users)	Pierre Letouzey	2017-05-22
*	romega: no more normalization trace, replaced by some Coq-side computation	Pierre Letouzey	2017-05-22
*	romega/const_omega : a few improvements (less try with, no gen equality)	Pierre Letouzey	2017-05-22
*	romega: use N instead of nat for Tvar	Pierre Letouzey	2017-05-22
*	romega: shorter trace (no more term lengths)	Pierre Letouzey	2017-05-22
*	refl_omega: refactoring of normalize_equation	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: lots of dead code + a few refactored proofs	Pierre Letouzey	2017-05-22
*	romega: if it bugs again, at least do it with a short and quick error	Pierre Letouzey	2017-05-22
*	refl_omega: comment the lack of lifts when dealing with arrows	Pierre Letouzey	2017-05-22
*	romega: discard constructor D_mono (shorter trace + fix a bug)	Pierre Letouzey	2017-05-22
*	refl_omega: more refactoring (e.g. IntSets instead of sorted lists)	Pierre Letouzey	2017-05-22
*	refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: discard useless cosntructor P_NOP	Pierre Letouzey	2017-05-22
*	ReflOmegaCore: revised proofs (mostly bullets instead of ;[\|\|\|])	Pierre Letouzey	2017-05-22