coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \
* \| \| \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| *	end of correction of bug 4306	Julien Forest	2017-04-04
\| \| \| *	Bad correction in previous commit	Julien Forest	2017-04-04
\| \| \| *	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest	2017-04-04
\| * \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\| \|\ \ \ \| \|/ / / \|/\| \| \|
\| * \| \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| * \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\| \|\ \ \
* \| \| \| \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
* \| \| \| \|	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
* \| \| \| \|	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
* \| \| \| \|	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin	2017-03-24
\| \|/ / / \|/\| \| \|
\| \| * \|	Improving the API of constrexpr_ops.mli.	Hugo Herbelin	2017-03-23
\| \|/ / \|/\| \|
* \| \|	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès	2017-03-23
* \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Merge PR#495: funind: Ignore missing info for current function	Maxime Dénès	2017-03-23
\| \|\ \
\| * \| \|	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès	2017-03-23
\| \| * \|	funind: Ignore missing info for current function	Tej Chajed	2017-03-22
\| \|/ /
* \| \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
\| \| *	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\| \| \|\ \| \|_\|/ \|/\| \|
\| \| *	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Funind API using EConstr.	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
\| \| *	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Equality API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Elim API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Hipattern API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Tacmach 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
\| \| *	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Evarconv 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
* \| \|	Extend Fast_typeops to be a replacement for Typeops	Gaetan Gilbert	2016-12-12
\| \|/ \|/\|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	That Function is unable to create a Fixpoint equation is a user problem,	Yves Bertot	2016-10-25
* \|	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
* \|	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
\|/ /
* \|	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \