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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
*
Miscellaneous typos, spacing, US spelling in comments or variable names.
Hugo Herbelin
2015-10-18
|
*
Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,
Hugo Herbelin
2015-10-18
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-10-16
|
\
|
*
|
Hashcons bytecode generated by the VM.
Pierre-Marie Pédrot
2015-10-16
*
|
Exporting a purely functional interface to bytecode patching.
Pierre-Marie Pédrot
2015-10-16
|
*
Remove left2right reference from the kernel.
Maxime Dénès
2015-10-16
|
*
Avoid dependency of the pretyper on C code.
Maxime Dénès
2015-10-15
|
*
Fix #4346 2/2: VM casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
|
*
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
|
*
Warn user when bytecode compilation fails.
Maxime Dénès
2015-10-15
|
*
Remove now useless exception handler in default conversion.
Maxime Dénès
2015-10-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Fix detection of ties in oracle_order.
Guillaume Melquiond
2015-10-15
|
*
Univs: inductives, remove unneeded test
Matthieu Sozeau
2015-10-14
|
*
Temporary fix: kernel conversion needs to ignore l2r flag.
Maxime Dénès
2015-10-14
|
*
Remove reference to default conversion function inside the kernel.
Maxime Dénès
2015-10-14
|
*
Remove -vm flag of coqtop.
Maxime Dénès
2015-10-14
|
*
Remove unused infos structure in VM.
Maxime Dénès
2015-10-14
|
*
Make interpreter of PROJ simpler by not using the stack.
Guillaume Melquiond
2015-10-14
|
*
Remove some unused variables.
Guillaume Melquiond
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-12
|
\
|
|
*
Univs: be more restrictive for template polymorphic constants: only
Matthieu Sozeau
2015-10-12
|
*
Gather VM tags in Cbytecodes.
Maxime Dénès
2015-10-12
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Complete handling of primitive projections in VM.
Maxime Dénès
2015-10-09
|
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
|
*
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
|
*
term_typing: strengthen discharging code
Enrico Tassi
2015-10-08
*
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
*
Univs: fix bug #4288, Print Sorted generated backward < constraints.
Matthieu Sozeau
2015-10-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
*
Univs: Change intf of push_named_def to return the computed universe
Matthieu Sozeau
2015-10-02
|
*
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
|
*
Univs: forgot a substitution in mod_typing.
Matthieu Sozeau
2015-10-02
|
*
Univs: correct handling of with in modules
Matthieu Sozeau
2015-10-02
|
*
Univs: fix bug #4251, handling of template polymorphic constants.
Matthieu Sozeau
2015-10-02
|
*
Univs: fix subtyping of polymorphic parameters.
Matthieu Sozeau
2015-10-02
|
*
Univs: uncovered bug in strengthening of opaque polymorphic definitions.
Matthieu Sozeau
2015-10-02
|
*
Univs: handle side-effects of futures correctly in kernel.
Matthieu Sozeau
2015-10-02
|
*
Univs (kernel) adapt to new invariants
Matthieu Sozeau
2015-10-02
|
*
Univs: module constraints move to universe contexts as they might
Matthieu Sozeau
2015-10-02
|
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
|
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
[next]