coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Library: use ocaml typing to show that we find at most 2 files	Gaëtan Gilbert	2018-07-03
*	Library.register_loaded_library: remove unused variable	Gaëtan Gilbert	2018-07-03
*	Libobject.apply_dyn_fun: remove unused deflt argument	Gaëtan Gilbert	2018-07-03
*	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
*	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\
\| *	Remove reference name type.	Maxime Dénès	2018-06-18
* \|	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\|/
*	Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...	Pierre-Marie Pédrot	2018-06-14
\|\
* \|	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: remove dummy alias.	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: module_kind to Declaremods	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: multi to tactics/rewrite	Emilio Jesus Gallego Arias	2018-06-12
* \|	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
\| *	Fixes #7192 (Print Assumptions does not enter implementation of submodules).	Hugo Herbelin	2018-04-07
* \|	[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
\|\ \ \