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
*	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
\| \| \| *	[general] Move Tactypes to `interp`	Emilio Jesus Gallego Arias	2017-11-01
\| \| \|/ \| \|/\|
\| \| *	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
\|/ /
* /	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\|/
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
* \|	[deps] Move `Discharge` to `interp`	Emilio Jesus Gallego Arias	2017-10-09
\| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
* \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
\| *	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
* \|	Reporting locations in error messages about notation formats.	Hugo Herbelin	2017-09-18
\|/
*	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès	2017-09-15
\|\
* \|	Adding a missing period in a notation warning.	Hugo Herbelin	2017-09-12
* \|	Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.	Hugo Herbelin	2017-09-12
* \|	Fixing a typo in printing notations with recursive binders.	Hugo Herbelin	2017-09-12
* \|	Fixing a bug of recursive notations introduced in dfdaf4de.	Hugo Herbelin	2017-09-12
* \|	Fixing little inaccuracy in coercions to ident or name.	Hugo Herbelin	2017-09-12
\| *	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\|/
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès	2017-08-31
\|\
* \	Merge PR #946: Functional pretyping interface	Maxime Dénès	2017-08-29
\|\ \
* \ \	Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...	Maxime Dénès	2017-08-29
\|\ \ \
* \ \ \	Merge PR #773: [flags] Remove XML output flag.	Maxime Dénès	2017-08-29
\|\ \ \ \
\| \| * \| \|	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29