coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \	Merge PR #6248: [api] Remove aliases of `Evar.t`	Maxime Dénès	2017-11-28
\|\ \
\| * \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
* \| \|	Use Evarutil.has_undefined_evars for tactic has_evar.	Gaëtan Gilbert	2017-11-24
\|/ /
\| *	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| *	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\|/
*	Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing	Maxime Dénès	2017-11-24
\|\
* \	Merge PR #486: Make some functions on terms more robust w.r.t new term constr...	Maxime Dénès	2017-11-24
\|\ \
* \ \	Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion	Maxime Dénès	2017-11-24
\|\ \ \
* \ \ \	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\ \ \ \
\| \| \| * \|	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
* \| \| \| \|	Merge PR #6186: [api] Miscellaneous consolidation.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| * \|	Recognizing Z in romega up to conversion.	Hugo Herbelin	2017-11-23
\| \| \| * \|	Using is_conv rather than eq_constr to find `nat` or `Z` in omega.	Hugo Herbelin	2017-11-23
\| \|_\|/ / \|/\| \| \|
\| \| \| *	Fixing a 8.7 regression of ring_simplify in ArithRing.	Hugo Herbelin	2017-11-23
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Maxime Dénès	2017-11-23
\|\ \ \
\| \| \| *	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
\| \|_\|/ \|/\| \|
\| \| *	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| \| *	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\| \|/ \|/\|
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
* \|	Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.	Maxime Dénès	2017-11-21
\|\ \
* \ \	Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses	Maxime Dénès	2017-11-21
\|\ \ \
\| * \| \|	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin	2017-11-20
* \| \| \|	Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.	Maxime Dénès	2017-11-20
\|\ \ \ \
* \ \ \ \	Merge PR #6161: Fix micromega.ml to match generated file and enforce match in...	Maxime Dénès	2017-11-20
\|\ \ \ \ \
\| \| \| \| \| *	Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Gaëtan Gilbert	2017-11-19
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| * \| \|	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias	2017-11-19
\| \|/ / / \|/\| \| \|
\| \| \| *	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias	2017-11-19
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.	Maxime Dénès	2017-11-16
\|\ \ \
* \ \ \	Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2	Maxime Dénès	2017-11-16
\|\ \ \ \
\| \| \| * \|	Fix micromega.ml to match generated file and enforce match in make.	Gaëtan Gilbert	2017-11-16
\| \|_\|/ / \|/\| \| \|
\| \| \| *	Fixing printing of tactics encapsulated as tacarg with Tacexp.	Hugo Herbelin	2017-11-15
\| \| \| *	Using "l" printer for glob_constr, like for constr.	Hugo Herbelin	2017-11-15
\| \|_\|/ \|/\| \|
\| \| *	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\| \|/ \|/\|
* \|	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\ \
\| * \|	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
* \| \|	Adding support for syntax "let _ := e in e'" in Ltac.	Hugo Herbelin	2017-11-04
\|/ /
* \|	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\ \
* \ \	Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).	Maxime Dénès	2017-11-03
\|\ \ \
\| \| * \|	Ltac Debug: exporting env and sigma when needed so that term can be printed.	Hugo Herbelin	2017-11-02
\| \| * \|	Binding ltac printing functions to the system of generic printing.	Hugo Herbelin	2017-11-02
\| \| * \|	Setting a system to register printers for Ltac values.	Hugo Herbelin	2017-11-02
\| \| * \|	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\| \| * \|	Exporting a few more printing functions.	Hugo Herbelin	2017-11-02
\| \| * \|	Improving checks about the list separator in tactic notations.	Hugo Herbelin	2017-11-02
\| \|/ / \|/\| \|
\| * \|	Fixing #2881 ("change with" failing in an Ltac definition).	Hugo Herbelin	2017-10-30
* \| \|	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès	2017-10-27
\|\ \ \