coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Proofview.Goal primitive 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
*	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Class_tactics 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
*	Hipattern 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
*	Refine 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
*	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping 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
*	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
*	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
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \|\
\| \| *	Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."	Maxime Dénès	2016-10-25
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \|
\| * \|	Fix bug #4464: "Anomaly: variable H' unbound. Please report.".	Pierre-Marie Pédrot	2016-10-07
* \| \|	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-10-02
\|\\| \| \|
\| * \| \|	Micro refactoring: use exact_no_check.	Théo Zimmermann	2016-10-01
\| * \| \|	Fix bug #5045: [generalize] creates ill-typed terms in 8.6.	Pierre-Marie Pédrot	2016-09-30
\| * \| \|	Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.	Pierre-Marie Pédrot	2016-09-30
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\| \| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-27
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| * \| \|	Moving "move" in the new proof engine.	Hugo Herbelin	2016-09-24
\| \| * \|	Ensuring that the evar name is preserved by "rename" as it is already	Hugo Herbelin	2016-09-24
* \| \| \|	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
* \| \| \|	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
* \| \| \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
\| * \| \|	Typo.	Hugo Herbelin	2016-09-15
\| \| \| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\| \| \|/ \| \|/\|
* \| \|	Removing the last uses of Pptactic in the lower layers.	Pierre-Marie Pédrot	2016-09-09
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|