diff options
Diffstat (limited to 'tactics')
| -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 d048d5bcdb..0c0204081a 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -726,7 +726,7 @@ let case_eq_intros_rewrite x = let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO (n'-n-1) intro; - Proofview.V82.tactic (Tacmach.introduction h); + introduction h; rewrite_except h] end ] |