diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v index c4594b6994149dc83c110564981ca799ff9309d0..b5602fbec04b654362c4508e17cbc82b986a87a4 100644 --- a/theories/proofmode/ltac_tactics.v +++ b/theories/proofmode/ltac_tactics.v @@ -601,7 +601,7 @@ Ltac iSpecializePat_go H1 pats := fail "iSpecialize:" H1 "not found" |solve_to_wand H1 |lazymatch m with - | GSpatial => notypeclasses refine (add_modal_id _ _) + | GSpatial => class_apply add_modal_id | GModal => iSolveTC || fail "iSpecialize: goal not a modality" end |pm_reflexivity ||