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-10-15
Correct some spelling errors
Benjamin Barenblat
2018-10-08
Merge PR #8654: Remove FCast from CClosure.fterm.
Maxime Dénès
2018-10-06
[api] Remove (most) 8.9 deprecated objects.
Emilio Jesus Gallego Arias
2018-10-05
[kernel] Remove section paths from `KerName.t`
Maxime Dénès
2018-10-04
Remove FCast from CClosure.fterm.
Pierre-Marie Pédrot
2018-10-02
Merge PR #8572: [config] Miscellaneous cleaning of configuration variables.
Pierre-Marie Pédrot
2018-10-02
Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0
Pierre-Marie Pédrot
2018-10-01
Merge PR #8254: Inline the definition of CClosure.mk_clos_deep.
Maxime Dénès
2018-10-01
Merge PR #8577: Generalize type of compare_head_with functions, and use for e...
Pierre-Marie Pédrot
2018-10-01
Merge PR #8575: Remove {Safe_typing,Global}.push_context
Maxime Dénès
2018-10-01
[nit] Qualify `Envars` use.
Emilio Jesus Gallego Arias
2018-09-28
Generalize type of compare_head_with functions
Gaëtan Gilbert
2018-09-27
[dune] [merlin] Fix some usability issues.
Emilio Jesus Gallego Arias
2018-09-27
Remove {Safe_typing,Global}.push_context
Gaëtan Gilbert
2018-09-27
Merge PR #8475: Centralize the reliance on abstract universe context internals
Gaëtan Gilbert
2018-09-26
[ocaml] Update required OCaml version to 4.05.0
Emilio Jesus Gallego Arias
2018-09-26
Inline the definition of CClosure.mk_clos_deep.
Pierre-Marie Pédrot
2018-09-26
Merge PR #8534: Checking if low-level name printers are used on purpose or not
Maxime Dénès
2018-09-24
[kernel] Compile with almost all warnings enabled.
Emilio Jesus Gallego Arias
2018-09-23
Checking if low-level name printers are used on purpose or not.
Hugo Herbelin
2018-09-21
Remove hash based univ level compare
Gaëtan Gilbert
2018-09-21
Fix printing of abstract universe contexts.
Pierre-Marie Pédrot
2018-09-19
Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)
Matthieu Sozeau
2018-09-19
Merge PR #8447: Cleaning in the retroknowledge
Pierre-Marie Pédrot
2018-09-17
Merge PR #6906: [VM] Optimize structured values
Pierre-Marie Pédrot
2018-09-17
Merge PR #8053: [dune] Add apidoc target using `odoc`
Gaëtan Gilbert
2018-09-17
OCaml now exports the min and max non-constant tags, let's use it
Maxime Dénès
2018-09-17
Add assertion on tags in eq_structured_constants
Maxime Dénès
2018-09-17
[VM] Allocate a bit less in digits_from_uint
Maxime Dénès
2018-09-17
[VM] Inject structured constants in values without reallocating them.
Maxime Dénès
2018-09-17
[VM] Move structured_constant to Vmvalues
Maxime Dénès
2018-09-14
Register: simpler syntax
Vincent Laporte
2018-09-14
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Vincent Laporte
2018-09-14
Retroknowledge: simpler parsing rules
Vincent Laporte
2018-09-14
Retroknowledge: remove the (unused) by clause
Vincent Laporte
2018-09-14
Retroknowledge.KInt31: remove the (unused) group parameter
Vincent Laporte
2018-09-13
Merge PR #8434: Canonical representation of kernel substitutions
Maxime Dénès
2018-09-13
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Maxime Dénès
2018-09-13
Do not catch already declared universes in Environ.add_universes
Gaëtan Gilbert
2018-09-13
Avoid repeat univ declaration in cumulative subtyping check
Gaëtan Gilbert
2018-09-13
Avoid repeat universe declarations for constants with split univs
Gaëtan Gilbert
2018-09-13
Kernel: fully obey mind_entry_template
Gaëtan Gilbert
2018-09-12
Fix mli-doc following #7109.
Théo Zimmermann
2018-09-12
Move maps & sets indexed by GlobRef.t into the kernel
Vincent Laporte
2018-09-12
Merge PR #8097: Use more efficient accu check for cofix unfolding in native c...
Maxime Dénès
2018-09-12
Merge PR #7109: Term combinators respecting the canonical structure of branch...
Maxime Dénès
2018-09-11
Merge PR #8278: Do not inline let-bound functions in clambda optimization.
Maxime Dénès
2018-09-10
[dune] Add apidoc target using `odoc`
Emilio Jesus Gallego Arias
2018-09-07
Canonical representation of kernel substitutions.
Pierre-Marie Pédrot
2018-09-07
Remove dead code in Mod_subst.
Pierre-Marie Pédrot
[next]