diff options
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 92cb8a11ea..af52c52370 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 |