coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| \| *	Forbid repeated names in universe binders.	Gaëtan Gilbert	2017-11-25
\| \| *	Universe binders survive sections, modules and compilation.	Gaëtan Gilbert	2017-11-25
\| \| *	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\| \| *	Make restrict_universe_context stronger.	Gaëtan Gilbert	2017-11-25
* \| \|	[lib] Generalize Control.timeout type.	Emilio Jesus Gallego Arias	2017-11-24
\|/ /
\| *	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| *	restrict_universe_context: do not prune named universes.	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
\| *	Use Maps and ids for universe binders	Gaëtan Gilbert	2017-11-24
\| *	Use type Universes.universe_binders.	Gaëtan Gilbert	2017-11-24
\|/
*	Merge PR #6203: Fix universe polymorphic Program obligations.	Maxime Dénès	2017-11-23
\|\
* \|	[api] A few more minor deprecation notices.	Emilio Jesus Gallego Arias	2017-11-22
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| *	Fix universe polymorphic Program obligations.	Matthieu Sozeau	2017-11-22
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
* \|	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias	2017-11-19
\|/
*	[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
*	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\
* \|	Cosmetic changes in evar_map printer.	Hugo Herbelin	2017-11-05
* \|	Preventively protect locally against failures of evar_map printer.	Hugo Herbelin	2017-11-05
* \|	Fixing a cause of failure of evar_map printer in debugger.	Hugo Herbelin	2017-11-05
\| *	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\|/
*	Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.	Maxime Dénès	2017-11-03
\|\
* \	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\ \
\| * \|	Exporting ValTMap for use in Genintern.	Hugo Herbelin	2017-11-02
\| \| *	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert	2017-11-01
\| \|/
* /	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin	2017-10-28
\|/
*	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\
* \	Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...	Maxime Dénès	2017-10-06
\|\ \
* \ \	Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...	Maxime Dénès	2017-10-05
\|\ \ \
* \ \ \	Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...	Maxime Dénès	2017-10-05
\|\ \ \ \
\| \| \| * \|	Fixing BZ#5769 (variable of type "_something" was named after invalid "_").	Hugo Herbelin	2017-10-05
\| \| \| \| *	Remove TODO comment (Evar.t is opaque)	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
\| \|_\|/ \|/\| \|
\| \| *	Moving setting of "cleared" evar flag directly in Evd.restrict.	Hugo Herbelin	2017-09-27
\| \| *	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
\| \|/ \|/\|
\| *	Fixing an old bug in collecting evars with cleared context.	Hugo Herbelin	2017-09-27
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \	Merge PR #1036: Unify EConstr.t equality	Maxime Dénès	2017-09-19
\|\ \
\| \| *	Document UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| *	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| *	proof_global: cleanup and comment close_proof	Matthieu Sozeau	2017-09-19