index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
Age
Commit message (
Expand
)
Author
2018-11-20
Use a closure for the domain argument of FProd.
Pierre-Marie Pédrot
2018-11-20
More efficient implementation of type_of_apply.
Pierre-Marie Pédrot
2018-11-20
Do not wrap FProd return types in a closure.
Pierre-Marie Pédrot
2018-11-20
Merge PR #7925: Clean transparent state
Maxime Dénès
2018-11-19
Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.
Pierre-Marie Pédrot
2018-11-19
Rename TranspState into TransparentState.
Pierre-Marie Pédrot
2018-11-19
Proper record type and accessors for transparent states.
Pierre-Marie Pédrot
2018-11-19
Move transparent_state to its own module.
Pierre-Marie Pédrot
2018-11-19
Merge PR #8451: Print Universes Subgraph
Pierre-Marie Pédrot
2018-11-16
Use universe names when printing to dot.
Gaëtan Gilbert
2018-11-16
Make UGraph printing independent of hash order
Gaëtan Gilbert
2018-11-16
We improve a little bit in printing universe constraints signature mismatch.
Hugo Herbelin
2018-11-16
Print full binders in subtyping incompatible polymorphism error.
Gaëtan Gilbert
2018-11-15
Make set_typing_flags "smart"
Gaëtan Gilbert
2018-11-09
Use arrays of names instead of lists in abstract universe names.
Pierre-Marie Pédrot
2018-11-09
Actually store the bound name information in the abstract universe context.
Pierre-Marie Pédrot
2018-11-09
Force the user to provide names when generating abstract universe contexts.
Pierre-Marie Pédrot
2018-11-09
Adding universe names to polymorphic entry instances.
Pierre-Marie Pédrot
2018-11-06
[checker] Refactor by sharing code with the kernel
Maxime Dénès
2018-11-06
Move debug term printer to kernel
Maxime Dénès
2018-11-05
Merge PR #8870: Pass native and VM flags to the kernel through environment
Pierre-Marie Pédrot
2018-11-05
Merge PR #8866: Check universe instances in Typing
Pierre-Marie Pédrot
2018-11-05
Merge PR #8824: Do not check convertibility of pattern types in the kernel
Maxime Dénès
2018-11-05
Pass native and VM flags to the kernel through environment
Maxime Dénès
2018-10-31
Use standard combinator for Global.set_strategy
Maxime Dénès
2018-10-31
Introduce Safe_typing.set_share_reduction
Maxime Dénès
2018-10-31
Seeing Global purely as a wrapper on top of kernel functions.
Hugo Herbelin
2018-10-31
Merge PR #8752: Enable fragile pattern warning in cclosure
Maxime Dénès
2018-10-30
Remove Environ.set_universes / Typing.enrich_env
Gaëtan Gilbert
2018-10-30
Check univ instances in Typing.
Gaëtan Gilbert
2018-10-30
Simplify universe handling in environ constant_type functions
Gaëtan Gilbert
2018-10-29
Do not compare the type arguments in pattern-match branches.
Pierre-Marie Pédrot
2018-10-29
Do not box fconstr closures in pattern-match branches.
Pierre-Marie Pédrot
2018-10-29
Integrate convert_shape into convert_stack.
Pierre-Marie Pédrot
2018-10-29
Merge PR #8780: Cleanup comparing projections through their constants.
Maxime Dénès
2018-10-26
Merge PR #8684: Remove a few circumvolutions around parameters of inductive e...
Gaëtan Gilbert
2018-10-26
Merge PR #8687: Mini reorganization type of global constr of global
Pierre-Marie Pédrot
2018-10-26
Merge PR #8814: Comment Environ.set_universes
Maxime Dénès
2018-10-26
Remove a few circumvolutions around parameters of inductive entries
Maxime Dénès
2018-10-26
Merge PR #8777: Move side-effects into Safe_typing
Maxime Dénès
2018-10-26
Merge PR #8707: Separate cache representation between CClosure and CBV
Maxime Dénès
2018-10-26
Merge PR #7186: Moving `fold_constr_with_full_binders` to a place
Maxime Dénès
2018-10-24
Comment Environ.set_universes
Gaëtan Gilbert
2018-10-22
Merge PR #8708: Stupid but critical unfolding heuristic.
Maxime Dénès
2018-10-20
Cleanup comparing projections through their constants.
Gaëtan Gilbert
2018-10-19
Moving Global.constr_of_global_in_context to Typeops.
Hugo Herbelin
2018-10-19
Moving Global.type_of_global_in_context to Typeops.
Hugo Herbelin
2018-10-19
Cleaning layout typeops.mli.
Hugo Herbelin
2018-10-19
Explicitly merge contexts in side-effect universe handling.
Pierre-Marie Pédrot
2018-10-19
Move side-effect typing into Safe_env.
Pierre-Marie Pédrot
[next]