coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
*	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
* \| \| \|	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