aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/ESpecialize.v
blob: 288bc8607aa7eb5d28e6bc143206ef8161a64a77 (plain) 
1
2

(** Like [specialize] but allows holes that get filled with evars. *)
Tactic Notation "especialize" open_constr(H) := specialize H.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 15:10:54 +0000