diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-22 17:12:58 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-06-14 07:19:50 +0200 |
| commit | daf5335b18c926d7130cd28e50f00cc49c4011f6 (patch) | |
| tree | f45377ea4597a3ba7699fa2e8b77046c7adc9b75 /tactics | |
| parent | 571c319ed536cb2757176d3ae4007a75f5d3b04d (diff) | |
Remove support for Coq 8.3.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 46c042b8b..5c2370253 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1416,7 +1416,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = "" else " You can try to use option Set Keep Proof Equalities." in tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) - | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> + | Inr [([],_,_)] -> tclZEROMSG (str"Nothing to inject.") | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns |