coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7215: Deprecate the "simple subst" tactic.	Hugo Herbelin	2018-04-16
\|\
* \	Merge PR #7200: [ltac] Deprecate nameless fix/cofix.	Maxime Dénès	2018-04-16
\|\ \
* \| \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
* \| \|	Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...	Pierre-Marie Pédrot	2018-04-13
\|\ \ \
\| \| * \|	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
\| \|/ / \|/\| \|
\| \| *	Deprecate the "simple subst" tactic.	Pierre-Marie Pédrot	2018-04-10
\| \|/ \|/\|
* \|	[api] Move some types to their proper module.	Emilio Jesus Gallego Arias	2018-04-02
* \|	Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of tclTHEN...	Pierre-Marie Pédrot	2018-04-01
\|\ \
\| \| *	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\| \|/ \|/\|
* \|	Fix #6631: Derive Plugin gives "Anomaly: more than one statement".	Pierre-Marie Pédrot	2018-03-29
\| *	Adding tacticals tclBINDFIRST/tclBINDLAST.	Hugo Herbelin	2018-03-27
\|/
*	Deprecate undocumented "intros until 0" in favor of "intros *".	Hugo Herbelin	2018-03-23
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
*	Add an invariant on given up goals in class_tactics.	Hugo Herbelin	2018-03-08
*	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
*	Proof engine: consider the pair principal and future goals as an entity.	Hugo Herbelin	2018-03-08
*	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \
* \ \ \	Merge PR #6924: Clean-up remove always false useeager argument.	Maxime Dénès	2018-03-08
\|\ \ \ \
* \ \ \ \	Merge PR #6902: [compat] Remove "Discriminate Introduction"	Maxime Dénès	2018-03-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6903: [compat] Remove "Shrink Abstract"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Clean-up remove always false useeager argument.	Théo Zimmermann	2018-03-06
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
\| \| \| \| \| \| *	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| * \| \|	[compat] Remove "Discriminate Introduction"	Emilio Jesus Gallego Arias	2018-03-06
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	[compat] Remove "Shrink Abstract"	Emilio Jesus Gallego Arias	2018-03-06
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\ \ \ \
* \ \ \ \	Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"	Maxime Dénès	2018-03-06
\|\ \ \ \ \
\| \| \| * \| \|	Tweak comments to fix ocamldoc errors	mrmr1993	2018-03-05
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \
\| \| \| \| * \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| * \| \| \| \|	tactics: export e_reduct_in_concl	Enrico Tassi	2018-03-04
* \| \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6676: [proofview] goals come with a state	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| *	[compat] Remove "Standard Proposition Elimination"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \| \| * \| \|	[compat] Remove "Injection L2R Pattern Order"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \|/\|
\| \| \| \| * \| / \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
\| \| \| \| \| \|/ / \| \| \| \| \|/\| \|
* \| \| \| / \| \|	Fixing rewriting in side conditions for "rewrite in " and "rewrite in \|-".	Hugo Herbelin	2018-03-01
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| * \| \| \|	Moving code for "simple induction"/"simple destruct" to coretactics.ml4.	Hugo Herbelin	2018-03-01
\| \|/ / / / \|/\| \| \| \|
\| \| * \| \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\| \|/ / / \|/\| \| \|
\| \| * \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|/ / \|/\| \|
* \| \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\| * \|	proofview: goals come with a state	Enrico Tassi	2018-02-20
\|/ /