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 PR #6666: Fix reduction of primitive projections on coinductive records...
Maxime Dénès
2018-01-30
|
\
*
\
Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections
Maxime Dénès
2018-01-30
|
\
\
|
|
*
[native_compute] Fix evaluation of cofixpoints under primitive projections.
Maxime Dénès
2018-01-29
*
|
|
Safer VM interfaces
Maxime Dénès
2018-01-26
|
|
/
|
/
|
|
*
Fix #6621: Anomaly on fixpoint with primitive projections
Maxime Dénès
2018-01-24
|
/
*
Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...
Maxime Dénès
2018-01-23
|
\
*
\
Merge PR #6506: Fast rel lookup
Maxime Dénès
2018-01-22
|
\
\
|
|
*
Remove dead code in Environ.
Pierre-Marie Pédrot
2018-01-20
|
|
/
|
/
|
*
|
Store the conversion oracle in constant and inductive definitions.
Pierre-Marie Pédrot
2018-01-14
*
|
Merge PR #6578: Remove references to deleted Unicode.Unsupported exception
Maxime Dénès
2018-01-13
|
\
\
*
|
|
Enforce that polymorphic definitions do not generate internal constraints.
Pierre-Marie Pédrot
2018-01-11
|
*
|
Remove references to removed Unicode.Unsupported
Jasper Hugunin
2018-01-11
|
/
/
*
|
Add a comment about universe lifting in sections in the kernel.
Pierre-Marie Pédrot
2017-12-31
*
|
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-12-30
*
|
Returning instance instead of substitution in universe context abstraction.
Pierre-Marie Pédrot
2017-12-30
*
|
Hardening universe abstraction in Cooking.
Pierre-Marie Pédrot
2017-12-30
|
*
Share the rel environment between Environ.env and reduction cache.
Pierre-Marie Pédrot
2017-12-29
|
*
Fast environment lookup for rels.
Pierre-Marie Pédrot
2017-12-29
|
/
*
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
*
Merge PR #6469: No universe constraints in Let definitions
Maxime Dénès
2017-12-22
|
\
*
\
Merge PR #6449: Let definitions must not contain side-effects when reaching t...
Maxime Dénès
2017-12-20
|
\
\
|
|
*
Let definitions do not create new universe constraints.
Pierre-Marie Pédrot
2017-12-19
|
|
*
Specific type for section definition entries.
Pierre-Marie Pédrot
2017-12-19
|
|
/
*
|
Fix order of let-in representation comment.
Jasper Hugunin
2017-12-19
|
*
Let definitions must not contain side-effects when reaching the kernel.
Pierre-Marie Pédrot
2017-12-16
|
/
*
Merge PR #6264: [kernel] Patch allowing to disable VM reduction.
Maxime Dénès
2017-12-14
|
\
*
\
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Maxime Dénès
2017-12-14
|
\
\
*
\
\
Merge PR #6368: [api] Remove yet another type alias.
Maxime Dénès
2017-12-11
|
\
\
\
*
|
|
|
[api] Remove kernel dependency on intf (Decl_kind)
Emilio Jesus Gallego Arias
2017-12-10
|
*
|
|
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
|
/
/
/
|
*
/
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
|
/
/
|
*
[kernel] Patch allowing to disable VM reduction.
Emilio Jesus Gallego Arias
2017-12-02
*
|
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
|
/
*
Fix native compute for byte compiled Coq.
Gaëtan Gilbert
2017-11-28
*
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-28
|
\
*
|
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
|
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
|
/
*
Merge PR #486: Make some functions on terms more robust w.r.t new term constr...
Maxime Dénès
2017-11-24
|
\
|
*
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-23
*
|
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
|
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
|
/
*
Merge PR #6058: Remove redundant env argument to Reduction.ccnv
Maxime Dénès
2017-11-15
|
\
*
|
[ci] [coq] Complete 4.06.0 support.
Emilio Jesus Gallego Arias
2017-11-13
*
|
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
|
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
|
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
|
*
Remove redundant env argument to Reduction.ccnv
Gaëtan Gilbert
2017-11-02
|
/
*
A missing newline after a comment.
Hugo Herbelin
2017-10-24
*
Merge PR #1155: Use type nonrec in some functor arguments.
Maxime Dénès
2017-10-20
|
\
*
|
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-10-17
[next]