index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
[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
*
|
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
*
|
Asserting that monomorphic section variables have no abstracted context.
Pierre-Marie Pédrot
2017-07-11
*
|
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
*
|
Removing a redundant universe instance information in native compute.
Pierre-Marie Pédrot
2017-07-10
*
|
Merge PR #853: Clean 'with Definition' implementation.
Maxime Dénès
2017-07-06
|
\
\
*
|
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
|
Removing dead code in Subtyping.
Pierre-Marie Pédrot
2017-07-04
|
*
|
Removing a few suspicious functions from the kernel.
Pierre-Marie Pédrot
2017-07-03
|
*
|
Do not add original constraints to the environment in 'with Definition' check.
Pierre-Marie Pédrot
2017-07-03
|
/
/
*
|
Fix a bug in cumulativity
Amin Timany
2017-06-16
[next]