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#602: Fix more warnings
Maxime Dénès
2017-05-03
|
\
*
\
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-03
|
\
\
|
|
*
Remove dead code in native compiler.
Maxime Dénès
2017-05-02
|
|
/
|
/
|
*
|
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-02
|
\
\
*
|
|
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
*
|
|
Fix for bug 5507. Mispelt de Bruijn.
Théo Zimmermann
2017-05-01
*
|
|
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-28
|
\
\
\
|
|
*
|
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
|
|
*
|
Remove some unused values and types
Gaetan Gilbert
2017-04-27
|
|
*
|
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-27
|
|
*
|
Locally disable some warnings.
Gaetan Gilbert
2017-04-27
|
|
/
/
|
/
|
|
*
|
|
COMMENT: Pre_env.env
Matej Kosik
2017-04-20
*
|
|
correcting a typo in a comment
Matej Kosik
2017-04-20
*
|
|
correcting comments in the "Context" module
Matej Kosik
2017-04-20
*
|
|
simplifying "Environ.push_named" function
Matej Kosik
2017-04-20
*
|
|
refactoring "Names.DirPath.is_empty" function
Matej Kosik
2017-04-20
*
|
|
refactoring "Names.DirPath.compare" function
Matej Kosik
2017-04-20
*
|
|
refactoring "Names.DirPath.equal" function
Matej Kosik
2017-04-20
*
|
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
\
\
*
\
\
\
Merge PR#441: Port Toplevel to the Stm API
Maxime Dénès
2017-04-12
|
\
\
\
\
|
*
|
|
|
[stm] Remove edit_id.
Emilio Jesus Gallego Arias
2017-04-12
*
|
|
|
|
Merge PR#549: Fast path in weak head reduction of applied atoms.
Maxime Dénès
2017-04-11
|
\
\
\
\
\
|
|
|
|
|
*
Update various comments to use "template polymorphism"
Gaetan Gilbert
2017-04-11
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR#537: Efficient side-effect abstraction
Maxime Dénès
2017-04-11
|
\
\
\
\
\
|
|
|
|
|
*
Documenting how the recursive indices of a fixpoint are computed.
Hugo Herbelin
2017-04-09
|
|
|
|
|
/
|
|
|
|
/
|
|
|
*
/
|
Fast path in weak head reduction of applied atoms.
Pierre-Marie Pédrot
2017-04-08
|
|
|
/
/
*
|
|
|
Merge branch 'master' into econstr
Pierre-Marie Pédrot
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-07
|
|
*
|
|
Documenting the fact terms are only hashconsed outside of a section.
Pierre-Marie Pédrot
2017-04-06
|
*
|
|
|
Merge PR#434: Optimizing array mapping in the kernel.
Maxime Dénès
2017-04-05
|
|
\
\
\
\
|
|
|
|
*
|
Fix substitution of abstracted lemmas.
Pierre-Marie Pédrot
2017-04-04
|
|
|
_
|
/
/
|
|
/
|
|
|
|
|
|
|
*
Fix bug #5435: [Eval native_compute in] raises anomaly.
Maxime Dénès
2017-04-04
*
|
|
|
|
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-03-31
|
|
|
*
|
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-27
|
|
|
/
/
|
|
/
|
|
*
|
|
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
\
|
|
|
|
*
|
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-24
|
|
\
\
\
|
|
|
|
/
|
|
|
/
|
|
|
*
|
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-23
|
|
\
|
|
|
*
|
|
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-22
|
|
\
\
\
\
|
|
|
|
*
|
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-21
|
|
\
\
\
\
|
|
|
|
*
|
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-20
[next]