aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-04-09 15:57:58 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-04-09 15:57:58 +0200
commitf9ef634e94c667641a9da12fa2b9f8e585d6d5c6 (patch)
tree469ec787483efde36b699fd54fb1ba225c57c76a /CHANGES
parent894c970093c2ac3abd5581d9df7bd424fcd577ba (diff)
parente739f16b0792545ec210008cdd6264614fe695e4 (diff)
Merge PR #7103: Fix #7101: STM delegation policy broken
# Conflicts: # CHANGES
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES9
1 files changed, 9 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 3994caef6..234d6c0db 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,15 @@ Tactic language
- Ltac backtraces now contain include trace information about tactics
called by OCaml-defined tactics.
+Changes from 8.8+beta1 to 8.8.0
+===============================
+
+Tools
+
+- Asynchronous proof delegation policy was fixed. Since version 8.7
+ Coq was ignoring previous runs and the -async-proofs-delegation-threshold
+ option did not have the expected behavior.
+
Changes from 8.7.2 to 8.8+beta1
===============================