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' into v8.6
Pierre-Marie Pédrot
2016-09-09
|
\
|
*
Restore native compiler optimizations after they were broken by 9e2ee58.
Maxime Dénès
2016-09-09
*
|
Remove useless debug code.
Guillaume Melquiond
2016-09-02
*
|
More efficient data structure to check if a native file is loaded.
Maxime Dénès
2016-09-01
*
|
Use a better data structure for VM compilation of free vars.
Pierre-Marie Pédrot
2016-08-22
*
|
Make code a bit clearer by removing optional argument.
Guillaume Melquiond
2016-08-10
*
|
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-26
|
\
|
|
*
Fix bug #4876: critical bug in guard condition checker.
Matthieu Sozeau
2016-07-25
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
|
*
Prevent unsafe overwriting of Required modules by toplevel library.
Maxime Dénès
2016-07-05
|
*
congruence: Restrict refreshing to Set
Matthieu Sozeau
2016-07-04
*
|
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Shrink Proofs/Obligations by default and deprecate
Matthieu Sozeau
2016-06-27
*
|
[feedback] Add optional ?loc parameter to loggers.
Emilio Jesus Gallego Arias
2016-06-25
*
|
Fix bug #4825: [clear] should not dependency-check hypotheses that come above...
Pierre-Marie Pédrot
2016-06-20
*
|
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
|
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
|
Adding a local type-in-type flag in kernel declarations.
Pierre-Marie Pédrot
2016-06-18
*
|
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
*
|
Adding a default safe set of kernel typing flags to Declareops.
Pierre-Marie Pédrot
2016-06-16
*
|
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
|
newring: fix for hack using evars as integers.
Matthieu Sozeau
2016-06-09
*
|
|
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
|
|
Please never mention .mli-only file in *.mllib (or future *.mlpack)
Pierre Letouzey
2016-06-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Fix potential race condition in vm_compute.
Guillaume Melquiond
2016-05-31
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
|
Checker: avoid using obsolete names from Names
Pierre Letouzey
2016-05-31
|
*
|
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
|
|
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
|
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-02
|
\
|
|
|
*
|
Fixing an incompatility introduced in a404360: kernel conversion was
Hugo Herbelin
2016-04-27
*
|
|
This is an attempt to clarify terminology in choosing variable names
Hugo Herbelin
2016-04-14
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
|
|
*
|
|
Remove int64 emulation in bytecode interpreter.
Maxime Dénès
2016-03-25
|
*
|
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
|
*
|
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2016-03-22
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-18
|
\
|
|
|
*
|
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
|
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
|
*
|
Hashconsing modules.
Pierre-Marie Pédrot
2016-03-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
|
*
|
This fix is probably not enough to justify that there are no problems with
Maxime Dénès
2016-03-04
|
*
|
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
|
ADD: Names.Name.is_{anonymous,name}
Matej Kosik
2016-02-18
[next]