coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6532: Fix mli-doc issue #6531	Maxime Dénès	2018-01-08
\|\
\| *	Fix mli-doc issue #6531	Tony Beta Lambda	2018-01-01
* \|	Using a dedicated type for Lib.abstr_info.	Pierre-Marie Pédrot	2017-12-30
\|/
*	Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.	Maxime Dénès	2017-12-27
\|\
* \	Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...	Maxime Dénès	2017-12-27
\|\ \
\| \| *	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| \|/ \|/\|
* \|	Merge PR #6469: No universe constraints in Let definitions	Maxime Dénès	2017-12-22
\|\ \
* \ \	Merge PR #6449: Let definitions must not contain side-effects when reaching t...	Maxime Dénès	2017-12-20
\|\ \ \
\| \| * \|	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot	2017-12-19
\| \| * \|	Specific type for section definition entries.	Pierre-Marie Pédrot	2017-12-19
\| \|/ /
* \| \|	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \ \
\| \| * \|	Let definitions must not contain side-effects when reaching the kernel.	Pierre-Marie Pédrot	2017-12-16
\| \|/ / \|/\| \|
* \| \|	Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`	Maxime Dénès	2017-12-15
\|\ \ \
\| \| * \|	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
\| \|/ /
* \| \|	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \
\| \| * \|	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| \|/ / \|/\| \|
\| * \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| * \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
* \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\|/ /
* \|	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès	2017-12-07
\|\ \
* \| \|	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
* \| \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\| \| *	Remove unused boolean from cl_context field of Typeclasses.typeclass	Gaëtan Gilbert	2017-11-30
* \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|/ \|/\|
\| *	Selecting which notation to print based on current stack of scope.	Hugo Herbelin	2017-11-27
* \|	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
* \|	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 #486: Make some functions on terms more robust w.r.t new term constr...	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
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\|/
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès	2017-11-21
\|\
* \	Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.	Maxime Dénès	2017-11-20
\|\ \
* \ \	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès	2017-11-20
\|\ \ \
\| \| \| *	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
\| \|_\|/ \|/\| \|
\| \| *	[lib] Minor pending cleanup to consolidate helper function.	Emilio Jesus Gallego Arias	2017-11-19
\| \|/ \|/\|
\| *	One more step in fixing #5762 ("where" clause).	Hugo Herbelin	2017-11-14
* \|	[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
\|\ \
* \ \	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\ \ \
* \ \ \	Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.	Maxime Dénès	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
\| \|/ \|/\|
* \|	[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
\|\ \ \
\| * \| \|	Do not identify a pre_ident as a string Ltac value.	Hugo Herbelin	2017-11-02