aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-11-04 18:00:18 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-11-05 10:08:20 +0100
commitd8baa76d86eaa691a5386669596a6004bb44bb7a (patch)
treec7008e731003ab9bef4ece94c7d85738fe402ad9
parentdc4200a1c0e37a600537fd1809377a3137ce0cc3 (diff)
More precise refine compatibility
-rw-r--r--tactics/tactics.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 92cb8a11e..af52c5237 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4975,7 +4975,8 @@ module New = struct
let reduce_after_refine =
let onhyps =
(** We reduced everywhere in the hyps before 8.6 *)
- if Flags.version_less_or_equal Flags.V8_5 then None
+ if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0
+ then None
else Some []
in
reduce