diff --git a/src/redprl/redprl.grm b/src/redprl/redprl.grm
index 3501c14d7..5053afd9d 100644
--- a/src/redprl/redprl.grm
+++ b/src/redprl/redprl.grm
@@ -144,6 +144,7 @@ end
  | tactic of ast
  | tactics of ast list
  | hypBindings of (string * P.param_sort) list
+ | multiHypBindings of (string * P.param_sort) list
  | atomicRawMultitac of ast
  | atomicMultitac of ast
  | rawMultitac of ast
@@ -374,7 +375,7 @@ atomicRawMultitac
   | MTAC_PROGRESS LBRACKET multitac RBRACKET (Ast.$$ (O.MONO O.MTAC_PROGRESS, [\ (([], []), multitac)]))
   | MTAC_REC VARNAME IN LBRACKET multitac RBRACKET (Ast.$$ (O.MONO O.MTAC_REC, [\ (([],[VARNAME]), multitac)]))
   | LBRACKET multitac RBRACKET (multitac)
-  | hypBindings LEFT_ARROW atomicRawMultitac SEMI multitac %prec LEFT_ARROW (Tac.makeSeq multitac hypBindings atomicRawMultitac)
+  | hypBindings LEFT_ARROW atomicRawMultitac SEMI multitac %prec LEFT_ARROW (Tac.makeSeq atomicRawMultitac hypBindings multitac)
   | atomicTac %prec SEMI (Ast.$$ (O.MONO O.MTAC_ALL, [\ (([],[]), atomicTac)]))
   | (Ast.$$ (O.MONO O.MTAC_ALL, [\ (([],[]), Ast.$$ (O.MONO O.RULE_ID, []))]))
 
@@ -387,10 +388,13 @@ rawMultitac
 
 multitac : rawMultitac (annotate (Pos.pos (rawMultitac1left fileName) (rawMultitac1right fileName)) rawMultitac)
 
+multiHypBindings
+  : VARNAME ([(VARNAME, P.HYP)])
+  | VARNAME COMMA hypBindings ((VARNAME, P.HYP) :: hypBindings)
 
 hypBindings
   : VARNAME ([(VARNAME, P.HYP)])
-  | VARNAME COMMA hypBindings ((VARNAME, P.HYP) :: hypBindings)
+  | LBRACKET multiHypBindings RBRACKET (multiHypBindings)
 
 rawTactic
   : multitac %prec SEMI (Tac.multitacToTac multitac)
diff --git a/test/success/primitive-sequencing.prl b/test/success/primitive-sequencing.prl
new file mode 100644
index 000000000..751a556a9
--- /dev/null
+++ b/test/success/primitive-sequencing.prl
@@ -0,0 +1,4 @@
+Thm PrimitiveSequencingTest : [bool -> bool -> bool true] by [
+  {x,y} <- auto;
+  hyp{y}
+].
\ No newline at end of file