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
2017-04-10
comments: corrected in the Context module
Matej Kosik
2017-04-10
simplify: Environ.push_named
Matej Kosik
2017-04-10
refactoring: Names.DirPath.is_empty
Matej Kosik
2017-04-10
refactoring: Names.DirPath.compare
Matej Kosik
2017-04-10
refactoring: Names.DirPath.equal
Matej Kosik
2017-04-07
Merge PR#519: Faster side effects
Maxime Dénès
2017-04-07
Inline the only use of hcons_j in Term_typing.
Pierre-Marie Pédrot
2017-04-06
Documenting the fact terms are only hashconsed outside of a section.
Pierre-Marie Pédrot
2017-04-05
Merge PR#434: Optimizing array mapping in the kernel.
Maxime Dénès
2017-03-27
More efficient check in validity of side-effects.
Pierre-Marie Pédrot
2017-03-27
Adding the size of the opaquetab in its representation.
Pierre-Marie Pédrot
2017-03-27
Fix hashconsing of terms in the kernel.
Pierre-Marie Pédrot
2017-03-24
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-23
Documenting the API of side-effects.
Pierre-Marie Pédrot
2017-03-23
Using a dedicated datastructure for side effect ordering.
Pierre-Marie Pédrot
2017-03-23
Making the side_effects type opaque.
Pierre-Marie Pédrot
2017-03-23
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-22
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-03-22
Merge PR#482: [toplevel] Remove unusable option -notop
Maxime Dénès
2017-03-21
Add a few comments in term_typing.ml.
Maxime Dénès
2017-03-21
Do not typecheck twice the type of opaque constants.
Maxime Dénès
2017-03-21
Merge PR#134: Enable `-safe-string`
Maxime Dénès
2017-03-20
In the Kami project, that causes a stack overflow in one of the example files
Paul Steckler
2017-03-20
[misc] Remove warnings about String.set
Emilio Jesus Gallego Arias
2017-03-14
[safe-string] Enable -safe-string !
Emilio Jesus Gallego Arias
2017-03-14
[safe_string] library/nameops
Emilio Jesus Gallego Arias
2017-03-14
[safe_string] kernel/cemitcodes
Emilio Jesus Gallego Arias
2017-03-14
[toplevel] Remove unusable option -notop
Emilio Jesus Gallego Arias
2017-03-14
[safe-string] kernel/nativevalues
Emilio Jesus Gallego Arias
2017-03-14
[safe_string] kernel/term_typing
Emilio Jesus Gallego Arias
2017-03-14
[future] Remove unused parameter greedy.
Emilio Jesus Gallego Arias
2017-02-20
Merge PR#189: Remove tabulation support from pretty-printing.
Maxime Dénès
2017-02-19
Optimizing array mapping in the kernel.
Pierre-Marie Pédrot
2017-02-08
Merge PR#393: Replace Typeops with Fast_typeops
Maxime Dénès
2017-02-01
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-01
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-01-28
Remove useless comments
Gaetan Gilbert
2017-01-26
[native comp] Improve error message on linking error.
Emilio Jesus Gallego Arias
2017-01-20
Do not add redundant side effects in tactic code.
Pierre-Marie Pédrot
2017-01-19
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-01-17
Mapping named_context_val preserves sharing when possible.
Pierre-Marie Pédrot
2016-12-26
Handle application of a primitive projection to a not yet evaluated cofixpoin...
Guillaume Melquiond
2016-12-23
Handle application of a primitive projection to a not yet evaluated cofixpoin...
Guillaume Melquiond
2016-12-22
Fixing injection in the presence of let-in in constructors.
Hugo Herbelin
2016-12-12
Replace Typeops by Fast_typeops
Gaetan Gilbert
2016-12-12
Extend Fast_typeops to be a replacement for Typeops
Gaetan Gilbert
2016-12-07
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-06
Fix #5248 - test-suite fails in 8.6beta1
Maxime Dénès
2016-12-04
Merge remote-tracking branch 'github/pr/366' into v8.6
Maxime Dénès
2016-12-02
Document changes
Matthieu Sozeau
[next]