diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index 19893d72..4eb0ef51 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -123,7 +123,7 @@ plain_topcomp:
   | HANDLE lst=top_handler_cases END                  { TopHandle lst }
   | DO c=term                                         { TopDo c }
   | FAIL c=term                                       { TopFail c }
-  | CONSTANT xs=nonempty_list(var_name) COLON u=term  { DeclConstants (xs, u) }
+  | CONSTANT xs=separated_nonempty_list(COMMA, var_name) COLON u=term  { DeclConstants (xs, u) }
   | MLTYPE lst=mlty_defs                              { DefMLType lst }
   | MLTYPE REC lst=mlty_defs                          { DefMLTypeRec lst }
   | OPERATION op=var_name COLON opsig=op_mlsig        { DeclOperation (op, opsig) }
diff --git a/tests/bad-congr.m31 b/tests/bad-congr.m31
index ca31bdea..a267d6d0 100644
--- a/tests/bad-congr.m31
+++ b/tests/bad-congr.m31
@@ -1,7 +1,7 @@
 
 fail congr_prod Type Type Type
 
-constant A B : Type
+constant A, B : Type
 
 fail congr_prod (assume x : A -> B in x) A (refl B)
 
diff --git a/tests/coerce.m31 b/tests/coerce.m31
index 69a68e37..0b06c094 100644
--- a/tests/coerce.m31
+++ b/tests/coerce.m31
@@ -1,4 +1,4 @@
-constant A B C : Type
+constant A, B, C : Type
 constant a : A
 constant f : A -> B
 constant g : B -> C
diff --git a/tests/dynamic.m31 b/tests/dynamic.m31
index c33e93a0..e5637a27 100644
--- a/tests/dynamic.m31
+++ b/tests/dynamic.m31
@@ -1,6 +1,6 @@
 
 constant A : Type
-constant a b : A
+constant a, b : A
 
 dynamic x = a
 
diff --git a/tests/error-context-subst.m31 b/tests/error-context-subst.m31
index cb6f63db..a3f6543d 100644
--- a/tests/error-context-subst.m31
+++ b/tests/error-context-subst.m31
@@ -1,6 +1,6 @@
 (* Substitute with different values in separate subterms, then join. *)
 
-constant A B C : Type
+constant A, B, C : Type
 constant pair : A -> B -> C
 
 let T = assume T : Type in T
diff --git a/tests/eta-pair.m31 b/tests/eta-pair.m31
index 96f8f4e5..0c8584c7 100644
--- a/tests/eta-pair.m31
+++ b/tests/eta-pair.m31
@@ -26,7 +26,7 @@ constant pair_eta :
 
 constant C : Type
 constant D : Type
-constant p q : prod C D
+constant p, q : prod C D
 
 
 (* Beta rules. *)
diff --git a/tests/everything.m31 b/tests/everything.m31
index 02ecaaaa..81de577d 100644
--- a/tests/everything.m31
+++ b/tests/everything.m31
@@ -17,9 +17,9 @@ operation nonary_op : color
 (** Declare constants *)
 (* constant `names` : `type` *)
 constant A : (* the type of types *) Type
-constant a b : A
+constant a, b : A
 (* Ocaml-style infixes are valid `name`s and `label`s *)
-constant ( + ) ( * ) ( ^ ) ( - ) ( <= ) :
+constant ( + ), ( * ), ( ^ ), ( - ), ( <= ) :
   (* non-dependent product type *) A -> A -> A
 
 (* Infixes and prefixes are printed as such. *)
diff --git a/tests/generic.m31 b/tests/generic.m31
index 9fff215f..ccc6da6b 100644
--- a/tests/generic.m31
+++ b/tests/generic.m31
@@ -1,5 +1,5 @@
 
-constant A B : Type
+constant A, B : Type
 constant eq : A == B
 now betas = add_beta eq
 
diff --git a/tests/handle-pattern-default.m31 b/tests/handle-pattern-default.m31
index 2f87af88..578dbc4b 100644
--- a/tests/handle-pattern-default.m31
+++ b/tests/handle-pattern-default.m31
@@ -2,7 +2,7 @@
 operation O : judgement -> mlstring
 
 constant A : Type
-constant a b : A
+constant a, b : A
 
 (* when an operation doesn't match, we need to bubble it upwards, then pass the result to the continuation *)
 do 
diff --git a/tests/implicit.m31 b/tests/implicit.m31
index f1dbe898..7076ade8 100644
--- a/tests/implicit.m31
+++ b/tests/implicit.m31
@@ -1,6 +1,6 @@
 constant A : Type
 constant a : A
-constant f g h : A -> A
+constant f, g, h : A -> A
 constant g_def : g == (lambda x : A, f (f x))
 constant h_def : h == g
 
diff --git a/tests/infixes.m31 b/tests/infixes.m31
index 4087413a..b4b4814c 100644
--- a/tests/infixes.m31
+++ b/tests/infixes.m31
@@ -2,9 +2,9 @@
 (** TT infixes *)
 constant A : Type
 
-constant a b c d : A
+constant a, b, c, d : A
 
-constant ( + ) ( - ) ( ^ ) ( / ) : A -> A -> A
+constant ( + ), ( - ), ( ^ ), ( / ) : A -> A -> A
 
 let s = (-) ((+) a b) ((^) c ((^) d d))
 
diff --git a/tests/many-constants-declaration.m31 b/tests/many-constants-declaration.m31
index 8a67bb40..bbaaa3d7 100644
--- a/tests/many-constants-declaration.m31
+++ b/tests/many-constants-declaration.m31
@@ -1,5 +1,5 @@
 (* Test whether declaration of several constants works. *)
-constant A B : Type
-constant f g : A -> Type
+constant A, B : Type
+constant f, g : A -> Type
 constant a : A
-constant x y z : f a -> Type
\ No newline at end of file
+constant x, y, z : f a -> Type
diff --git a/tests/natural.m31 b/tests/natural.m31
index e1b743f9..e1801a08 100644
--- a/tests/natural.m31
+++ b/tests/natural.m31
@@ -1,4 +1,4 @@
-constant A B : Type
+constant A, B : Type
 constant a : A
 constant eq : A == B
 
@@ -18,4 +18,4 @@ do
     natural (f a : (a == a))
   with
   | coerce (|- _ : C a) (|- a == a) => yield (Convertible xi)
-  end
\ No newline at end of file
+  end
diff --git a/tests/unhandled-op.m31 b/tests/unhandled-op.m31
index 5e2e1890..e57f7df8 100644
--- a/tests/unhandled-op.m31
+++ b/tests/unhandled-op.m31
@@ -2,7 +2,7 @@
 mltype x = x end
 
 constant A : Type
-constant a b : A
+constant a, b : A
 constant (+) : A -> A -> A
 
 operation Not_found : empty