diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index bce768cd4..d048d5bcd 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -706,7 +706,7 @@ let mkCaseEq a : unit Proofview.tactic = let env = Proofview.Goal.env gl in Proofview.V82.tactic begin change_concl - (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl) + (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)) end end; simplest_case a] |