coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| *	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Cleaning up interfaces.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Removing compatibility layers related to printing.	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
\| \| \| *	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
\| \| \| *	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Class_tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Leminv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Inv 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
\| \| \| *	Tacmach 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
\| \| \| *	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Classops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Typeclasses 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
\| \| \| *	Recordops 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
\| \| \| *	Cbv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Nativenorm API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| \| *	Vnorm 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 PR#393: Replace Typeops with Fast_typeops	Maxime Dénès	2017-02-08
\|\ \ \ \
* \ \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\|\ \ \ \ \ \| \| \|_\|/ / \| \|/\| \| \|
* \| \| \| \|	Adding a new evar source to remember the name of evars which were	Hugo Herbelin	2017-01-22
\| * \| \| \|	Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).	Hugo Herbelin	2017-01-22
\| \| \| * \|	Improve unification debug trace.	Théo Zimmermann	2016-12-13
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Replace Typeops by Fast_typeops	Gaetan Gilbert	2016-12-12
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\|\\| \|
\| * \|	Merge remote-tracking branch 'github/pr/366' into v8.6	Maxime Dénès	2016-12-04
\| \|\ \