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-10-26
|
\
|
*
Fix #5127 Memory corruption with the VM
Maxime Dénès
2016-10-24
*
|
More comments in VM.
Maxime Dénès
2016-10-19
*
|
Remove dead code in Environ.
Pierre-Marie Pédrot
2016-10-12
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
*
Fix for bug #4863, update the Proofview's env with
Matthieu Sozeau
2016-10-11
*
|
Removing a slow access to a named environment.
Pierre-Marie Pédrot
2016-10-06
*
|
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
\
\
*
\
\
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-09
|
\
\
\
|
|
|
/
|
|
/
|
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
|
*
|
Restore native compiler optimizations after they were broken by 9e2ee58.
Maxime Dénès
2016-09-09
|
|
*
Removing the now useless field env_named_val from named_context_val.
Pierre-Marie Pédrot
2016-09-09
|
|
*
More efficient implementation of map_named_val.
Pierre-Marie Pédrot
2016-09-09
|
|
*
Fast access environment in CClosure.
Pierre-Marie Pédrot
2016-09-09
|
|
*
Tentative fast-access named env
Pierre-Marie Pédrot
2016-09-09
|
|
*
Packing the named_context_val in a proper record and marking it private.
Pierre-Marie Pédrot
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
|
\
|
|
[next]