coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.	Maxime Dénès	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
\|\ \ \
\| \| \| *	[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: 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
\|\ \ \ \ \ \
\| \| \| \| \| \| *	[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
* \| \| \|	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
* \| \| \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| \|_\|/ \|/\| \|
\| * \|	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\|/ /
* \|	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\ \
* \ \	Merge PR #6648: [tactics] make apply_type safe	Maxime Dénès	2018-02-19
\|\ \ \
* \ \ \	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...	Maxime Dénès	2018-02-19
\|\ \ \ \
* \ \ \ \	Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.	Maxime Dénès	2018-02-19
\|\ \ \ \ \
\| \| * \| \| \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| * \| \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| \|_\|/ / / \|/\| \| \| \|
\| \| \| \| *	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \ \
* \ \ \	Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...	Maxime Dénès	2018-02-05
\|\ \ \ \
\| \| * \| \|	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
\| \|/ / / \|/\| \| \|
\| * \| \|	[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition	Vincent Laporte	2018-02-01
* \| \| \|	Delete duplicate line	Paul Steckler	2018-01-30
\|/ / /
\| * /	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/ /
* \|	Remove dead code from funind.	Maxime Dénès	2018-01-24
* \|	Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.	Maxime Dénès	2018-01-18
\|\ \
\| * \|	Use let-in aware prod_applist_assum in dtauto and firstorder.	Jasper Hugunin	2018-01-17
* \| \|	Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr	Maxime Dénès	2018-01-16
\|\ \ \
* \ \ \	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
\| \| * \|	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08