coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Notations: Do not consider a non-occurring variable as a binder-only variable.	Hugo Herbelin	2018-02-20
*	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
*	Adding support for re-folding notation referring to isolated "forall '(x,y), t".	Hugo Herbelin	2018-02-20
*	Again one more step in fixing #5762 ("where" clause).	Hugo Herbelin	2018-02-20
*	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
*	Merge PR #1047: Support universe instances on the literal Type	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès	2018-02-12
\|\ \
\| * \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
\| * \|	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert	2018-02-10
\| * \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
* \| \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/ /
\| *	Support universe instances on the literal Type	Tej Chajed	2018-01-26
\|/
*	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
\| \|_\|/ \|/\| \|