coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\
* \	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
\|\ \ \
\| \| * \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
* \| \| \|	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
*	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\
* \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\|/
*	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
*	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
*	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\
* \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
* \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \| *	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \| *	Remove deprecated option Dependent Propositions Eliminiation.	Théo Zimmermann	2017-12-11
\| \|/ \|/\|
\| *	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\|/
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	[api] Insert miscellaneous API deprecation back to core.	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
*	Update tactics.ml	Farzon Lotfi	2017-11-02
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Moving bug numbers to BZ# format in the source code.	Théo Zimmermann	2017-10-19
*	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\
\| *	Remove a failwith ""	Gaëtan Gilbert	2017-09-29
* \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
* \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\|/
*	Merge PR #1060: An optimization of tactic constructor	Maxime Dénès	2017-09-25
\|\
* \|	Mark "Set Tactic Compat Context" as deprecated.	Guillaume Melquiond	2017-09-21
\| *	An optimization of tactic constructor.	Hugo Herbelin	2017-09-19
\|/
*	Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).	Maxime Dénès	2017-09-19
\|\
* \	Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...	Maxime Dénès	2017-09-15
\|\ \
\| \| *	Avoid extra failure in the "constructor" tactic (bug #5666).	Guillaume Melquiond	2017-09-14
\| \|/ \|/\|
\| *	Fixing part of #5707 (allowing destruct to use non dependent case analysis).	Hugo Herbelin	2017-08-30
* \|	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\ \
* \ \	Merge PR #805: Functional tactics	Maxime Dénès	2017-08-29
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).	Maxime Dénès	2017-08-01
\|\ \ \
\| \| * \|	Replacing tclENV with the goal environment	amblaf	2017-07-31
\| \| * \|	Remove references to Global.env in tactics/*.ml	amblaf	2017-07-31
\| \|/ / \|/\| \|
\| * \|	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin	2017-07-27
* \| \|	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
\|/ /