diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-02-20 16:03:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-02 23:45:51 +0100 |
| commit | 3ce123f16ce19f67dde4a0f3f2874a2678649907 (patch) | |
| tree | 1357c6556ba947f066c16a1aa946c7e2ddb399d4 /tactics/contradiction.ml | |
| parent | a4817d25befc71b7dbf707637660431144985133 (diff) | |
Remove 8.5 compatibility support.
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 467754a84..3386f972e 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 _ -> |