add make_simple_intropattern

It's not needed for !512 (merged) after all, but could still be useful in the future.

stdpp/tactics.v

@@ -266,6 +266,11 @@ unifies a successor. *)
 Tactic Notation "eunify" open_constr(x) open_constr(y) :=
   unify x y.
 
+(** [make_simple_intropattern] provides a way to write a term that is
+interpreted as a [simple_intropattern]. This works around the lack of
+[simple_intropattern:(...)] in ltac's syntax. *)
+Tactic Notation "make_simple_intropattern" simple_intropattern(pat) := pat.
+
 (** Operational type class projections in recursive calls are not folded back
 appropriately by [simpl]. The tactic [csimpl] uses the [fold_classes] tactics
 to refold recursive calls of [fmap], [mbind], [omap] and [alter]. A