coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
\| \|/
* \|	Fix order of let-in representation comment.	Jasper Hugunin	2017-12-19
\| *	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 #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \
* \ \	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \
* \| \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| * \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\|/ / /
\| * /	[lib] Rename Profile to CProfile	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
\|/
*	Fix native compute for byte compiled Coq.	Gaëtan Gilbert	2017-11-28
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	When declaring constants/inductives use ContextSet if monomorphic.	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
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\|/
*	Merge PR #6058: Remove redundant env argument to Reduction.ccnv	Maxime Dénès	2017-11-15
\|\
* \|	[ci] [coq] Complete 4.06.0 support.	Emilio Jesus Gallego Arias	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
\| *	Remove redundant env argument to Reduction.ccnv	Gaëtan Gilbert	2017-11-02
\|/
*	A missing newline after a comment.	Hugo Herbelin	2017-10-24
*	Merge PR #1155: Use type nonrec in some functor arguments.	Maxime Dénès	2017-10-20
\|\
* \|	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
\| *	Use type nonrec in some functor arguments.	Gaëtan Gilbert	2017-10-16
\|/
*	Merge PR #1103: Take Suggest Proof Using outside the kernel.	Maxime Dénès	2017-10-13
\|\
\| *	Take Suggest Proof Using outside the kernel.	Gaëtan Gilbert	2017-10-10
* \|	[flambda] [native] Pass `-Oclassic` to the native compiler.	Emilio Jesus Gallego Arias	2017-10-10
\|/
*	Merge PR #1109: Handle some misc todos	Maxime Dénès	2017-10-09
\|\
* \|	[stm] [flags] Move document mode flags to the STM.	Emilio Jesus Gallego Arias	2017-10-06
\| *	Remove unused Failure catch	Gaëtan Gilbert	2017-09-29
\| *	Remove some duplication between Typeops and Nativenorm.	Gaëtan Gilbert	2017-09-29
* \|	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot	2017-09-28
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
\| *	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
* \|	Merge PR #920: kernel: bugfix in filter_stack_domain.	Maxime Dénès	2017-09-19
\|\ \ \| \|/ \|/\|
* \|	Merge PR #955: Do not hashcons universes beforehand	Maxime Dénès	2017-09-15
\|\ \
* \ \	Merge PR #931: Parametrize module body	Maxime Dénès	2017-09-07
\|\ \ \
\| \| * \|	Do not hashcons universes beforehand.	Pierre-Marie Pédrot	2017-09-01
\| \|/ / \|/\| \|
* \| \|	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès	2017-08-31
\|\ \ \
\| \| * \|	Statically enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot	2017-08-29
\| \| * \|	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29