coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	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
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).	Guillaume Melquiond	2016-05-02
* \|	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	Using monotonic types for conversion functions.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \|	CLEANUP: in the Reductionops module	Matej Kosik	2015-12-17
* \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \|	More efficient implementation of equality-up-to-universes in Universes.	Pierre-Marie Pédrot	2015-11-26
\|/
*	Fixing kernel bug in typing match with let-ins in the arity.	Hugo Herbelin	2015-11-22
*	Pushing the backtrace in conversion anomalies.	Pierre-Marie Pédrot	2015-11-09
*	Conversion of polymorphic inductive types was incomplete in VM and native.	Maxime Dénès	2015-10-28
*	Avoid dependency of the pretyper on C code.	Maxime Dénès	2015-10-15
*	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
*	Hopefully clearer printing of stack when debugging evarconv unification.	Hugo Herbelin	2015-08-02
*	Fix incompleteness of conversion used by evarconv	Matthieu Sozeau	2015-06-28
*	Fix bug #3532, providing universe inconsistency information when a	Matthieu Sozeau	2015-03-04
*	Fix bug #4103: forgot to allow unfolding projections of cofixpoints like	Matthieu Sozeau	2015-03-03
*	simpl: honor Global for "simpl: never" (Close: 3206)	Enrico Tassi	2015-02-27
*	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
*	Fixing bug #3071.	Pierre-Marie Pédrot	2015-02-21
*	Fix 'don't expose cases' in cbn	Pierre Boutillier	2015-02-15
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Option -type-in-type continued (deactivate test for inferred sort of	Hugo Herbelin	2014-11-19
*	Evar normalization is now done eagerly.	Pierre-Marie Pédrot	2014-11-10
*	Implement a different strategy to expand primitive projections only when	Matthieu Sozeau	2014-10-15