16 files changed, 26 insertions, 26 deletions

diff --git a/test/c/cheri128_hsb.sail b/test/c/cheri128_hsb.sail
index a06a2ad2..d8501d88 100644
--- a/test/c/cheri128_hsb.sail
+++ b/test/c/cheri128_hsb.sail
@@ -14,7 +14,7 @@ val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_
 val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
-val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
+val min = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c == 'a | 'c == 'b) & 'c <= 'a & 'c <= 'b . atom('c)}
 
 overload operator + = {add_range}
 overload operator - = {sub_range}
diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail
index 6d0bdaad..c4989829 100644
--- a/test/c/poly_pair.sail
+++ b/test/c/poly_pair.sail
@@ -4,7 +4,7 @@ val print = "print_endline" : string -> unit
 
 val "eq_int" : (int, int) -> bool
 
-union test ('a : Type) ('b : Type) = {
+union test('a : Type, 'b : Type) = {
   Ctor1 : ('a, 'b),
   Ctor2 : int
 }
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index d0a14586..f162d3a2 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -33,7 +33,7 @@ overload _mod_GPR = { rGPR, wGPR }
 /* Create a new type which is a pair of a bitvector and a start index
 
    slice('n, 'm) is equivalent to old-sail vector('n, 'm, dec, bit) */
-newtype slice ('n : Int) ('m : Int) = MkSlice : (atom('n), bits('m))
+newtype slice ('n : Int, 'm : Int) = MkSlice : (atom('n), bits('m))
 
 /* Extract the bitvector from a slice */
 val slice_bits : forall 'n 'm. slice('n, 'm) -> bits('m)
@@ -76,7 +76,7 @@ overload _mod_slice = {_set_slice, _set_slice2, vector_slice, slice_slice}
 /* Set up a struct with an aliased LT bit in CR0, mimicing old-style syntax */
 infix 1 ...
 
-type operator ... ('n : Int) ('m : Int) = slice('m, 'n - ('m - 1))
+type operator ...('n : Int, 'm : Int) = slice('m, 'n - ('m - 1))
 
 struct cr = {
   CR0 : 7 ... 4,
diff --git a/test/ocaml/void/void.sail b/test/ocaml/void/void.sail
index 485ac019..4e8815f5 100644
--- a/test/ocaml/void/void.sail
+++ b/test/ocaml/void/void.sail
@@ -1,5 +1,5 @@
 
-val void : forall 'n, 'n = 'n + 1. atom('n) -> unit
+val void : forall 'n, 'n == 'n + 1. atom('n) -> unit
 
 function void _ = ()
 
diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail
index c442d6a8..ae340941 100644
--- a/test/typecheck/pass/bind_typ_var.sail
+++ b/test/typecheck/pass/bind_typ_var.sail
@@ -1,7 +1,7 @@
 
 val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)}
 
-val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
+val mk_square : unit -> {'n 'm, 'n == 'm. vector('n, dec, vector('m, dec, bit))}
 
 val test : unit -> unit
 
@@ -10,8 +10,8 @@ function test () = {
   // could still be
   let v2 as 'len2 = mk_vector ();
   let matrix as vector('width, _, 'height) = mk_square ();
-  _prove(constraint('width = 'height));
-  _prove(constraint('len = 32 | 'len = 64));
-  _prove(constraint('len2 = 32 | 'len2 = 64));
+  _prove(constraint('width == 'height));
+  _prove(constraint('len == 32 | 'len == 64));
+  _prove(constraint('len2 == 32 | 'len2 == 64));
   ()
 }
\ No newline at end of file
diff --git a/test/typecheck/pass/constrained_struct.sail b/test/typecheck/pass/constrained_struct.sail
index 64b2287f..87d55b65 100644
--- a/test/typecheck/pass/constrained_struct.sail
+++ b/test/typecheck/pass/constrained_struct.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-struct MyStruct 'n, 'n in {32, 64} = {
+struct MyStruct('n), 'n in {32, 64} = {
   field: bits('n)
 }
 
diff --git a/test/typecheck/pass/constrained_struct/v1.sail b/test/typecheck/pass/constrained_struct/v1.sail
index 62fc1c01..98daf59e 100644
--- a/test/typecheck/pass/constrained_struct/v1.sail
+++ b/test/typecheck/pass/constrained_struct/v1.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-struct MyStruct 'n, 'n in {32, 64} = {
+struct MyStruct('n), 'n in {32, 64} = {
   field: bits('n)
 }
 
diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail
index ffa6d033..3e2acf28 100644
--- a/test/typecheck/pass/exint.sail
+++ b/test/typecheck/pass/exint.sail
@@ -1,8 +1,8 @@
 type MyInt = {'n, true. atom('n)}
 
-val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n + 'm. atom('o)}
+val add : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n + 'm. atom('o)}
 
-val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = 'n * 'm. atom('o)}
+val mult : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == 'n * 'm. atom('o)}
 
 overload operator + = {add}
 
@@ -14,7 +14,7 @@ let y = x + x * x
 
 let z : atom(7 * 8) = y
 
-type Range ('n : Int) ('m : Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
+type Range('n: Int, 'm: Int), 'n <= 'm = {'o, 'n <= 'o & 'o <= 'm. atom('o)}
 
 let a : Range(3, 4) = 3
 
diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail
index f6c0c073..6db518e8 100644
--- a/test/typecheck/pass/exist1.sail
+++ b/test/typecheck/pass/exist1.sail
@@ -22,6 +22,6 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
 let v8 = s_add(v7, 4)
diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail
index 42ec8cb1..102a1084 100644
--- a/test/typecheck/pass/exist2.sail
+++ b/test/typecheck/pass/exist2.sail
@@ -22,13 +22,13 @@ function unit_fn x : atom(4) = ()
 
 val s_add : forall 'a. (atom('a), atom('a)) -> atom('a + 'a)
 
-let v7 : {'k, 'k = 4. atom('k)} = 4
+let v7 : {'k, 'k == 4. atom('k)} = 4
 
-let v9 : {'n, 0 = 0. atom('n)} = 100
+let v9 : {'n, 0 == 0. atom('n)} = 100
 
 let v10 : int = v9
 
-type MyInt = {'n, 0 = 0. atom('n)}
+type MyInt = {'n, 0 == 0. atom('n)}
 
 val existential_int : int -> MyInt
 
@@ -37,7 +37,7 @@ val existential_range : forall 'n 'm.
 
 overload existential = {existential_int, existential_range}
 
-let v11 : {'n, 0 = 0. atom('n)} = existential(v10)
+let v11 : {'n, 0 == 0. atom('n)} = existential(v10)
 
 let v12 : {'e, 0 <= 'e & 'e <= 3. atom('e)} = existential(2 : range(0, 3))
 
diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail
index 44382213..b251cbf8 100644
--- a/test/typecheck/pass/exist_synonym.sail
+++ b/test/typecheck/pass/exist_synonym.sail
@@ -1,6 +1,6 @@
 
 // Type synonym with a constraint.
-type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+type regno('n: Int), 0 <= 'n < 32 = atom('n)
 
 // Existential with constrained type synonym.
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
index 3169f619..583c4485 100644
--- a/test/typecheck/pass/exist_synonym/v1.expect
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -2,6 +2,6 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char
 
 let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
 
-Tried performing type coercion from int(4) to {'n, 0 <= 'n & 'n <= 33. regno('n)} on 4
+Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4
 Failed because
 Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33)
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
index 02b1c17a..baddbcb0 100644
--- a/test/typecheck/pass/exist_synonym/v2.expect
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -2,6 +2,6 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char
 
 let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
 
-Tried performing type coercion from int(4) to {'n, 0 <= 'n & 'n <= 8. regno('n)} on 4
+Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4
 Failed because
 Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail
index 24e50259..ec4e72db 100644
--- a/test/typecheck/pass/option_either.sail
+++ b/test/typecheck/pass/option_either.sail
@@ -1,6 +1,6 @@
 default Order inc
 
-union option ('a : Type) = {None : unit, Some : 'a}
+union option('a: Type) = {None : unit, Some : 'a}
 
 function none forall ('a : Type). () -> option('a) = None()
 
@@ -11,7 +11,7 @@ function test forall ('a : Type). x : option('a) -> range(0, 1) = match x {
   Some(y) => 1
 }
 
-union either ('a : Type) ('b : Type) = {Left : 'a, Right : 'b}
+union either('a: Type, 'b: Type) = {Left : 'a, Right : 'b}
 
 val signed : forall ('n : Int), 'n >= 0. vector('n, inc, bit) -> int
 
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index cbdb2c9d..588fd324 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index cd3e849a..de388c3e 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -1,6 +1,6 @@
 default Order dec
 
-struct State ('a : Type) ('n : Int) = {
+struct State('a: Type, 'n: Int) = {
   N : vector('n, dec, 'a),
   Z : vector(1, dec, bit)
 }