coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
*	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
* \| \| \|	Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170	Maxime Dénès	2017-08-29
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
\| \| * \|	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin	2017-08-29
\| \|/ / \|/\| \|
\| * \|	Add native compute profiling, BZ#5170	Paul Steckler	2017-08-17
* \| \|	Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.	Hugo Herbelin	2017-08-12
\|/ /
* \|	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \
\| * \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| *	kernel: bugfix in filter_stack_domain.	Matthieu Sozeau	2017-07-26
\| \|/
* \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
* \|	Avoiding a variable shadowing in the kernel.	Pierre-Marie Pédrot	2017-07-26
* \|	Statically ensuring that inlined entries out of the kernel have no effects.	Pierre-Marie Pédrot	2017-07-26
* \|	Further simplication: do not recreate entries for side-effects.	Pierre-Marie Pédrot	2017-07-26
* \|	Remove a horrendous hack in Declare to retrieve exported side-effects.	Pierre-Marie Pédrot	2017-07-26
* \|	More precise type of entries capturing their lack of side-effects.	Pierre-Marie Pédrot	2017-07-26
* \|	Using a record type for Cooking.result.	Pierre-Marie Pédrot	2017-07-26
* \|	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
\|/
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[api] Put modules in order in API.{mli,ml}	Emilio Jesus Gallego Arias	2017-07-25
*	Merge PR #783: Remove some useless code in Term_typing	Maxime Dénès	2017-07-17
\|\
* \|	The only abstraction-breaking function in Univ is now AUContext.instance.	Pierre-Marie Pédrot	2017-07-13
* \|	Adding a comment regarding De Bruijn universe indices in the kernel.	Pierre-Marie Pédrot	2017-07-12
* \|	Moving the last bits of abtraction-breaking code out of the kernel.	Pierre-Marie Pédrot	2017-07-11
* \|	Fix nonsensical universe abstraction in the kernel.	Pierre-Marie Pédrot	2017-07-11
* \|	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
* \|	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
* \|	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11