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-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
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-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Introducing contexts parameterized by the inner term type.
Pierre-Marie Pédrot
2017-02-14
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
Making judgment type generic over the type of inner constrs.
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
2016-12-02
Merge remote-tracking branch 'github/pr/377' into v8.6
Maxime Dénès
2016-12-02
Fix #5242 - Dubious unsilenceable warning on invalid identifier
Maxime Dénès
2016-11-30
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-30
Univs: fix bug #5180
Matthieu Sozeau
2016-11-30
Fix UGraph.check_eq!
Matthieu Sozeau
2016-11-30
Slightly more efficient [Univ.super] implem
Matthieu Sozeau
2016-11-24
Fix incorrect long multiplication in the VM.
Guillaume Melquiond
2016-11-08
Introducing a new EConstr.t type to perform the nf_evar operation on demand.
Pierre-Marie Pédrot
[next]