coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
*	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	Statically enforce that ULub is only between levels.	Gaëtan Gilbert	2018-03-09
*	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
*	Proof engine: adding a function to save future goals including principal one.	Hugo Herbelin	2018-03-08
*	Proof engine: consider the pair principal and future goals as an entity.	Hugo Herbelin	2018-03-08
*	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\
\| *	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
* \|	Add empty description for @raise statements to satisfy ocamldoc	mrmr1993	2018-03-05
* \|	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\|/
*	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 #6275: [summary] Allow typed projections from global state.	Maxime Dénès	2017-12-12
\|\
* \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| *	[summary] Adapt STM to the new Summary API.	Emilio Jesus Gallego Arias	2017-12-09
\|/
*	Merge PR #1033: Universe binder improvements	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
\| *	Use Entries.constant_universes_entry more.	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
\|/
*	[api] A few more minor deprecation notices.	Emilio Jesus Gallego Arias	2017-11-22
*	[api] Insert miscellaneous API deprecation back to core.	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 #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\
\| *	Remove TODO comment (Evar.t is opaque)	Gaëtan Gilbert	2017-09-29
* \|	Moving setting of "cleared" evar flag directly in Evd.restrict.	Hugo Herbelin	2017-09-27
\|/
*	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
*	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \|\
\| * \|	Univs: fix bug #5365, generation of u+k <= v constraints	Matthieu Sozeau	2017-06-05
\| \| *	Bump year in headers.	Maxime Dénès	2017-06-01
\| \|/
* \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \|	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\ \
\| * \|	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
* \| \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\| \|
* \| \|	Making Evd independent from Namegen.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Chasing a few unsafe constr coercions.	Pierre-Marie Pédrot	2017-02-14
* \| \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14