coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\
* \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
\| *	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
* \|	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias	2018-05-30
* \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
\|/
*	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
*	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\
* \	Merge PR #7340: Remove DirClosedSection.	Enrico Tassi	2018-05-11
\|\ \
* \ \	Merge PR #7341: Don't recurse into closed modules/sections in split_lib.	Enrico Tassi	2018-05-11
\|\ \ \
\| \| \| *	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
\| \|_\|/ \|/\| \|
* \| \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
\| * \|	Don't recurse into closed modules/sections in split_lib.	Jasper Hugunin	2018-04-24
\|/ /
\| *	Remove DirClosedSection.	Jasper Hugunin	2018-04-24
\|/
*	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias	2018-04-23
*	[api] Remove dependency of library on Vernacexpr.	Emilio Jesus Gallego Arias	2018-04-06
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\
\| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
* \|	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	2018-03-09
* \|	Export the various option localities in the API.	Pierre-Marie Pédrot	2018-03-09
\|/
*	Use a proper warning when a summary is captured out of module scope.	Vincent Laporte	2018-03-07
*	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
*	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
*	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
*	Returning instance instead of substitution in universe context abstraction.	Pierre-Marie Pédrot	2017-12-30
*	Using a dedicated type for Lib.abstr_info.	Pierre-Marie Pédrot	2017-12-30
*	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 #6284: Warning for absolute name masking (deprecated, should become ...	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 #6264: [kernel] Patch allowing to disable VM reduction.	Maxime Dénès	2017-12-14
\|\ \
* \ \	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
\| * \| \|	[summary] Allow typed projections from global state + rework of internals.	Emilio Jesus Gallego Arias	2017-12-09
\|/ / /
\| * \|	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
* \| \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\|/ /
* \|	Merge PR #1049: Remove obsolete locality	Maxime Dénès	2017-11-30
\|\ \
\| \| *	Warning for absolute name masking (making it deprecated, should become	Matthieu Sozeau	2017-11-30
\| * \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|/
* /	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\|/
*	[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
*	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
*	[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
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\