coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
*	Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.	Hugo Herbelin	2018-05-23
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
*	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
*	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	2018-03-09
\| \| *	Statically enforce that ULub is only between levels.	Gaëtan Gilbert	2018-03-09
\| \| *	Option for messing with inference of irrelevant constraints	Gaëtan Gilbert	2018-03-09
\| \| *	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
\| \| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
\| \|/ \|/\|
* \|	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
* \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \
* \| \|	reductionops: remove dead code "bind_assum"	Enrico Tassi	2018-03-04
\| \| *	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot	2018-03-04
\| \|/ \|/\|
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	[get_cumulativity_constraints] allowing further code sharing.	Gaëtan Gilbert	2018-02-10
*	Factorize code for comparing maybe-cumulative inductives.	Gaëtan Gilbert	2018-02-10
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	Using a dedicated type for Lib.abstr_info.	Pierre-Marie Pédrot	2017-12-30
*	Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...	Maxime Dénès	2017-12-14
\|\
* \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
\| \| *	Further clean-up in Reductionops, removing unused lift arguments.	Maxime Dénès	2017-12-12
\| \|/ \|/\|
* \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| *	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\|/
*	Getting rid of the Update constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
*	Getting rid of the Shift constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
*	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
* \	Merge PR #6117: Fix printing anomaly in conv	Maxime Dénès	2017-11-13
\|\ \
\| * \|	Fixing missing separator in an error message.	Hugo Herbelin	2017-11-08
\| \| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|/ \|/\|
* \|	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\|/
*	Using EConstr equality check in unification.	Pierre-Marie Pédrot	2017-09-08
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	Merge branch 'v8.7'	Maxime Dénès	2017-07-20
\|\
\| *	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
* \|	Less footguns in universe handling: remove subst_instance_context.	Pierre-Marie Pédrot	2017-07-11
* \|	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Use inductive subtyping for conv/cumul	Amin Timany	2017-06-16
*	Merge PR#714: Print feature Proof-of-Concept (episode 2)	Maxime Dénès	2017-06-13
\|\
* \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\ \