1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v
index 97f3042d2b..910b6d5463 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -42,6 +42,16 @@ Ltac2 rec repeat0 (t : unit -> unit) :=
 
 Ltac2 Notation repeat := repeat0.
 
+Ltac2 dispatch0 t ((head, tail)) :=
+  match tail with
+  | None => Control.enter (fun _ => t (); Control.dispatch head)
+  | Some tacs =>
+    let ((def, rem)) := tacs in
+    Control.enter (fun _ => t (); Control.extend head def rem)
+  end.
+
+Ltac2 Notation t(thunk(self)) ">" "[" l(dispatch) "]" : 4 := dispatch0 t l.
+
 Ltac2 do0 n t :=
   let rec aux n t := match Int.equal n 0 with
   | true => ()