coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \
* \| \|	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
\| \| *	Added support for a side effect on constants in reduction functions.	Thomas Sibut-Pinote	2017-06-04
* \| \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| \|/ \|/\|
* \|	Merge PR#670: Postponing of universe constraints unification in term equality.	Maxime Dénès	2017-06-01
\|\ \
* \| \|	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \| \|	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| * \|	Postponing of universe constraints unification in term equality.	Pierre-Marie Pédrot	2017-05-23
\|/ /
* \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
* \|	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| *	Reinstate fixpoint refolding in [cbn], deactivated by mistake.	Matthieu Sozeau	2017-04-13
* \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\ \
* \| \|	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Cc API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
* \| \|	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Cleaning up opening of the EConstr module in pretyping folder.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| * \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\|/\| \| \| \|/
\| *	Univs: fix bug #5180	Matthieu Sozeau	2016-11-30
* \|	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Remove incorrect assertion in cbn (bug #4822).	Guillaume Melquiond	2016-09-28
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\\|
\| *	no-refold patch	Paul Steckler	2016-09-09
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \| \|/ \|/\|
\| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \|	[pp] Fix newline issues.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Make semantics of whd_zeta consistent with other whd_* functions.	Maxime Dénès	2016-07-01
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31