@@ -1146,13 +1146,13 @@ let rec get_case : type a b e.
11461146 (b, a) ty_sel -> (string * (e, b) ty_case) list -> string * (a, e) ty option =
11471147 fun sel cases ->
11481148 match cases with
1149- | (name, TCnoarg sel') :: rem -> begin
1150- match eq_sel sel sel' with
1149+ | (name, TCnoarg sel') :: rem ->
1150+ begin match eq_sel sel sel' with
11511151 | None -> get_case sel rem
11521152 | Some Eq -> name, None
11531153 end
1154- | (name, TCarg (sel', ty)) :: rem -> begin
1155- match eq_sel sel sel' with
1154+ | (name, TCarg (sel', ty)) :: rem ->
1155+ begin match eq_sel sel sel' with
11561156 | None -> get_case sel rem
11571157 | Some Eq -> name, Some ty
11581158 end
@@ -1214,8 +1214,8 @@ let rec devariantize : type t e. e ty_env -> (t, e) ty -> variant -> t =
12141214 | Econs (t, e') -> devariantize e' t v)
12151215 | Conv (s, proj, inj, t), VConv (s', v) when s = s' ->
12161216 inj (devariantize e t v)
1217- | Sum ops, VSum (tag, a) -> begin
1218- try
1217+ | Sum ops, VSum (tag, a) ->
1218+ begin try
12191219 match List.assoc tag ops.sum_cases, a with
12201220 | TCarg (sel, t), Some a -> ops.sum_inj (sel, devariantize e t a)
12211221 | TCnoarg sel, None -> ops.sum_inj (sel, Noarg)
@@ -1558,8 +1558,8 @@ let rec sameNat : type a b. a nat -> b nat -> (a, b) equal option =
15581558 fun a b ->
15591559 match a, b with
15601560 | NZ, NZ -> Some Eq
1561- | NS a', NS b' -> begin
1562- match sameNat a' b' with
1561+ | NS a', NS b' ->
1562+ begin match sameNat a' b' with
15631563 | Some Eq -> Some Eq
15641564 | None -> None
15651565 end
@@ -1754,13 +1754,13 @@ let rec del : type n. int -> n avl -> n avl_del =
17541754 | Node (bal, l, x, r) ->
17551755 if x = y then begin
17561756 match r with
1757- | Leaf -> begin
1758- match bal with
1757+ | Leaf ->
1758+ begin match bal with
17591759 | Same -> Ddecr (Eq, l)
17601760 | More -> Ddecr (Eq, l)
17611761 end
1762- | Node _ -> begin
1763- match bal, del_min r with
1762+ | Node _ ->
1763+ begin match bal, del_min r with
17641764 | _, (z, Inr r) -> Dsame (Node (bal, l, z, r))
17651765 | Same, (z, Inl r) -> Dsame (Node (More, l, z, r))
17661766 | Less, (z, Inl r) -> Ddecr (Eq, Node (Same, l, z, r))
@@ -1773,8 +1773,8 @@ let rec del : type n. int -> n avl -> n avl_del =
17731773 else if y < x then begin
17741774 match del y l with
17751775 | Dsame l -> Dsame (Node (bal, l, x, r))
1776- | Ddecr (Eq, l) -> begin
1777- match bal with
1776+ | Ddecr (Eq, l) ->
1777+ begin match bal with
17781778 | Same -> Dsame (Node (Less, l, x, r))
17791779 | More -> Ddecr (Eq, Node (Same, l, x, r))
17801780 | Less ->
@@ -1786,8 +1786,8 @@ let rec del : type n. int -> n avl -> n avl_del =
17861786 else begin
17871787 match del y r with
17881788 | Dsame r -> Dsame (Node (bal, l, x, r))
1789- | Ddecr (Eq, r) -> begin
1790- match bal with
1789+ | Ddecr (Eq, r) ->
1790+ begin match bal with
17911791 | Same -> Dsame (Node (More, l, x, r))
17921792 | Less -> Ddecr (Eq, Node (Same, l, x, r))
17931793 | More ->
@@ -1914,16 +1914,16 @@ let rec rep_equal : type a b. a rep -> b rep -> (a, b) equal option =
19141914 match ra, rb with
19151915 | Rint, Rint -> Some Eq
19161916 | Rbool, Rbool -> Some Eq
1917- | Rpair (a1, a2), Rpair (b1, b2) -> begin
1918- match rep_equal a1 b1 with
1917+ | Rpair (a1, a2), Rpair (b1, b2) ->
1918+ begin match rep_equal a1 b1 with
19191919 | None -> None
19201920 | Some Eq ->
19211921 match rep_equal a2 b2 with
19221922 | None -> None
19231923 | Some Eq -> Some Eq
19241924 end
1925- | Rfun (a1, a2), Rfun (b1, b2) -> begin
1926- match rep_equal a1 b1 with
1925+ | Rfun (a1, a2), Rfun (b1, b2) ->
1926+ begin match rep_equal a1 b1 with
19271927 | None -> None
19281928 | Some Eq ->
19291929 match rep_equal a2 b2 with
@@ -2033,8 +2033,8 @@ let rec compare : type a b. a rep -> b rep -> (string, (a, b) equal) sum =
20332033 fun a b ->
20342034 match a, b with
20352035 | I, I -> Inr Eq
2036- | Ar (x, y), Ar (s, t) -> begin
2037- match compare x s with
2036+ | Ar (x, y), Ar (s, t) ->
2037+ begin match compare x s with
20382038 | Inl _ as e -> e
20392039 | Inr Eq ->
20402040 match compare y t with
@@ -2073,23 +2073,23 @@ let rec tc : type n e. n nat -> e ctx -> term -> e checked =
20732073 fun n ctx t ->
20742074 match t with
20752075 | V s -> lookup s ctx
2076- | Ap (f, x) -> begin
2077- match tc n ctx f with
2076+ | Ap (f, x) ->
2077+ begin match tc n ctx f with
20782078 | Cerror _ as e -> e
20792079 | Cok (f', ft) ->
20802080 match tc n ctx x with
20812081 | Cerror _ as e -> e
20822082 | Cok (x', xt) ->
20832083 match ft with
2084- | Ar (a, b) -> begin
2085- match compare a xt with
2084+ | Ar (a, b) ->
2085+ begin match compare a xt with
20862086 | Inl s -> Cerror s
20872087 | Inr Eq -> Cok (App (f', x'), b)
20882088 end
20892089 | _ -> Cerror "Non fun in Ap"
20902090 end
2091- | Ab (s, t, body) -> begin
2092- match tc (NS n) (Ccons (n, s, t, ctx)) body with
2091+ | Ab (s, t, body) ->
2092+ begin match tc (NS n) (Ccons (n, s, t, ctx)) body with
20932093 | Cerror _ as e -> e
20942094 | Cok (body', et) -> Cok (Abs (n, body'), Ar (t, et))
20952095 end
@@ -2180,8 +2180,8 @@ let rec rule : type a b.
21802180 (pval, closed, (a, b) tarr) lam -> (pval, closed, a) lam -> b rlam =
21812181 fun v1 v2 ->
21822182 match v1, v2 with
2183- | Lam (x, body), v -> begin
2184- match subst body (Bind (x, v, Id)) with
2183+ | Lam (x, body), v ->
2184+ begin match subst body (Bind (x, v, Id)) with
21852185 | Ex term ->
21862186 match mode term with
21872187 | Pexp -> Inl term
@@ -2193,13 +2193,13 @@ let rec onestep : type m t. (m, closed, t) lam -> t rlam = function
21932193 | Const (r, v) -> Inr (Const (r, v))
21942194 | App (e1, e2) ->
21952195 match mode e1, mode e2 with
2196- | Pexp, _ -> begin
2197- match onestep e1 with
2196+ | Pexp, _ ->
2197+ begin match onestep e1 with
21982198 | Inl e -> Inl (App (e, e2))
21992199 | Inr v -> Inl (App (v, e2))
22002200 end
2201- | Pval, Pexp -> begin
2202- match onestep e2 with
2201+ | Pval, Pexp ->
2202+ begin match onestep e2 with
22032203 | Inl e -> Inl (App (e1, e))
22042204 | Inr v -> Inl (App (e1, v))
22052205 end
0 commit comments