coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6496: Generate typed generic code from ltac macros	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\ \ \
\| \| \| *	Make most of TACTIC EXTEND macros runtime calls.	Maxime Dénès	2018-03-08
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6918: romega: get rid of EConstr.Unsafe	Maxime Dénès	2018-03-08
\|\ \ \
* \ \ \	Merge PR #6909: Deprecate Focus and Unfocus	Maxime Dénès	2018-03-08
\|\ \ \ \
* \ \ \ \	Merge PR #6934: Warn when using “Require” in a section	Maxime Dénès	2018-03-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \
\| \| * \| \| \| \|	[stdlib] Do not use “Require” inside sections	Vincent Laporte	2018-03-07
\| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6932: [stdlib] Do not use deprecated notations	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| *	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| *	Extraction: switch to EConstr.t as the central type to extract from.	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| * \| \|	romega: get rid of EConstr.Unsafe	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \|/\|
\| \| \| * \| \| / \|	[stdlib] Do not use deprecated notations	Vincent Laporte	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
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \
\| \| \| \| * \| \|	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
* \| \| \| \| \| \|	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Escape curly braces in ocamldoc comment	mrmr1993	2018-03-05
\| \| \| \| \| * \| \|	Separate vim/emacs fold markers from ocamldoc comments	mrmr1993	2018-03-05
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| \| \| * \| \| \|	[ssreflect] Export parsing witnesses in mli file.	Emilio Jesus Gallego Arias	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
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
\| \| \| \| * \| \|	ssr: add Prenex Implicits for Some_inj to use it as a view	Anton Trunov	2018-03-04
\| \| \| \| * \| \|	ssr: fix typo in doc comment	Anton Trunov	2018-03-04
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| * \| \| \| \|	ssr: ipats: V82.tactic ~nf_evars:false everywhere	Enrico Tassi	2018-03-04
\| * \| \| \| \|	ssr: rewrite Ssripats and Ssrview in the tactic monad	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
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Remove all uses of Focus in standard library.	Théo Zimmermann	2018-03-04
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	[compat] Remove "Intuition Iff Unfolding"	Emilio Jesus Gallego Arias	2018-03-03
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| * \|	Turn warning for deprecated notations on.	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
\| \|/ / \|/\| \|
* \| \|	Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...	Maxime Dénès	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 #6604: Extend `zify_N` with knowledge about `N.pred`	Maxime Dénès	2018-02-21
\|\ \ \
* \ \ \	Merge PR #6767: [ci] add elpi	Maxime Dénès	2018-02-21
\|\ \ \ \
\| \| \| \| *	proofview: goals come with a state	Enrico Tassi	2018-02-20
\| \| \| * \|	Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).	Hugo Herbelin	2018-02-20
\| \| \| \|/
* \| \| \|	Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.	Hugo Herbelin	2018-02-20
* \| \| \|	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20