diff options
| author | Maxime Dénès | 2018-03-04 17:24:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 17:24:59 +0100 |
| commit | 78551857a41a57607ecfb3fd010e0a9755f47cea (patch) | |
| tree | 431275a5729dddb5ca4fa2d9199b8640aa4f45af /tactics | |
| parent | dffc6a20eb1a0636904164e00b5963ed96f774c4 (diff) | |
| parent | 2f60c1bab0ce391aa60cc6c387b9d36a1ae70905 (diff) | |
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 6 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
3 files changed, 3 insertions, 13 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 467754a848..3386f972e7 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -44,8 +44,6 @@ let absurd c = absurd c (* Contradiction *) -let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 - (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function @@ -71,9 +69,7 @@ let contradiction_context = simplest_elim (mkVar id) else match EConstr.kind sigma typ with | Prod (na,t,u) when is_empty_type sigma u -> - let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t - else None in + let is_unit_or_eq = match_with_unit_or_eq_type sigma t in Tacticals.New.tclORELSE (match is_unit_or_eq with | Some _ -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 32563d9ffc..96a53a8b1e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,7 +84,7 @@ let _ = let injection_in_context = ref false let use_injection_in_context = function - | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5 + | None -> !injection_in_context | Some flags -> flags.injection_in_context let _ = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 94622114dd..61ca3e319c 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 <*> |