coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was added	Maxime Dénès	2018-05-25
\|\
* \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
\| *	[ssr] fix after to_constr ~abort_on_undefined_evars was added	Enrico Tassi	2018-05-16
* \|	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert	2018-05-14
\|/
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Merge PR #7237: [ssr] fix delayed clears (fix #7045)	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
\|\ \
\| \| *	[ssr] fix delayed clears (fix #7045)	Enrico Tassi	2018-04-13
\| \|/ \|/\|
* \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	2018-04-04
\| *	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias	2018-03-31
\|/
*	Fix #7026: ssr: applying an overloaded lemma as a view takes too long.	Pierre-Marie Pédrot	2018-03-21
*	[ssreflect] Fix module scoping problems due to packing and mli files.	Emilio Jesus Gallego Arias	2018-03-10
*	[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
*	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	2018-03-09
*	Merge PR #6893: Cleanup UState API usage	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
\|\ \
* \ \	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
\|\ \ \ \
\| \| \| \| *	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
\|\ \ \ \ \ \| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| \| *	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
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
* \| \|	[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
*	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
*	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
\|/
*	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\
\| *	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
\|/
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	Merge PR #6219: Document undocumented options	Maxime Dénès	2017-12-15
\|\
\| *	Deprecate dead option Match Strict (ssr).	Gaëtan Gilbert	2017-12-14