coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
*	Removing compatibility layers in Retyping	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
*	Tactics 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
*	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
*	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacred 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
*	Evardefine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Find_subterm 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
*	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\
\| *	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\| \|\
\| \| *	Revert "unification.ml: fix for bug #4763, unif regression"	Maxime Dénès	2016-10-21
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-08
\| \|\\|
\| \| *	w_merge: Add a comment about the (List.rev evars)	Matthieu Sozeau	2016-10-06
\| \| *	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau	2016-10-06
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\| \|
\| * \|	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\| \|\ \
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| \| * \|	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\\| \| \|
\| * \| \|	no-refold patch	Paul Steckler	2016-09-09
\| \| \| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\| \| \|/ \| \|/\|
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \ \ \	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
* \| \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| * \| \|	Pushing error backtrace in unification reraise.	Pierre-Marie Pédrot	2016-08-22
\|/ / /
\| * \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| * \|	Remove errorlabstrm in favor of user_err	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
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
* \|	A mini-optimization for free in unification.ml: test in O(1)	Hugo Herbelin	2016-06-10
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20