coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Goal 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
*	Making judgment type generic over the type of inner constrs.	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
*	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacred API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Constr_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Patternops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Retyping 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
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\
\| *	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\| \|\
\| * \	Merge commit 'a799600' into v8.6	Maxime Dénès	2016-10-25
\| \|\ \
\| \| * \|	That Function is unable to create a Fixpoint equation is a user problem,	Yves Bertot	2016-10-25
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \| \|
\| * \| \|	ssrmatching: fix interpretation of rpattern	Enrico Tassi	2016-10-24
\| \|/ /
* \| \|	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
\| \| *	[pp] Use more convenient pp API in ssrmatching	Emilio Jesus Gallego Arias	2016-10-18
\| \| *	[pp] Add tagging function to all low-level printing calls.	Emilio Jesus Gallego Arias	2016-10-18
\| \|/
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\|
\| *	Fix bug #5023: JSON extraction doesn't generate "for xxx".	Pierre-Marie Pédrot	2016-10-17
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Ncring_initial: avoid a notation overriding	Pierre Letouzey	2016-09-29
\| *	Extraction: ignore some useless stuff about universes	Pierre Letouzey	2016-09-29
\| *	Ring_theory: avoid overriding a few notations	Pierre Letouzey	2016-09-28
\| *	Adding interface files to Nsatz ML files.	Pierre-Marie Pédrot	2016-09-28
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\|
\| *	Fast russian peasant exponentiation in Nsatz.	Pierre-Marie Pédrot	2016-09-26
\| *	Monomorphizing various uses of arrays in Nsatz.	Pierre-Marie Pédrot	2016-09-26
\| *	Partial fix for bug #5085: nsatz_compute stack overflows.	Pierre-Marie Pédrot	2016-09-26
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\|
* \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \|	Merge remote-tracking branch 'github/pr/283' into trunk	Maxime Dénès	2016-09-22
\|\ \
* \| \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\| * \|	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
\|/ /
\| *	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
* \|	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\ \
\| * \|	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| * \|	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
\| \| *	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08