diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 94622114d..61ca3e319 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5121,16 +5121,10 @@ module New = struct open Locus let reduce_after_refine = - let onhyps = - (** We reduced everywhere in the hyps before 8.6 *) - if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0 - then None - else Some [] - in reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; rZeta=false;rDelta=false;rConst=[]}) - {onhyps; concl_occs=AllOccurrences } + {onhyps = Some []; concl_occs = AllOccurrences } let refine ~typecheck c = Refine.refine ~typecheck c <*> |