diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-11-04 18:00:18 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-05 10:08:20 +0100 |
| commit | d8baa76d86eaa691a5386669596a6004bb44bb7a (patch) | |
| tree | c7008e731003ab9bef4ece94c7d85738fe402ad9 | |
| parent | dc4200a1c0e37a600537fd1809377a3137ce0cc3 (diff) | |
More precise refine compatibility
| -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 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 |