@@ -1148,13 +1148,13 @@ let rec get_case : type a b e.
11481148 (b, a) ty_sel -> (string * (e, b) ty_case) list -> string * (a, e) ty option =
11491149 fun sel cases ->
11501150 match cases with
1151- | (name, TCnoarg sel') :: rem -> begin
1152- match eq_sel sel sel' with
1151+ | (name, TCnoarg sel') :: rem ->
1152+ begin match eq_sel sel sel' with
11531153 | None -> get_case sel rem
11541154 | Some Eq -> name, None
11551155 end
1156- | (name, TCarg (sel', ty)) :: rem -> begin
1157- match eq_sel sel sel' with
1156+ | (name, TCarg (sel', ty)) :: rem ->
1157+ begin match eq_sel sel sel' with
11581158 | None -> get_case sel rem
11591159 | Some Eq -> name, Some ty
11601160 end
@@ -1216,8 +1216,8 @@ let rec devariantize : type t e. e ty_env -> (t, e) ty -> variant -> t =
12161216 | Econs (t, e') -> devariantize e' t v)
12171217 | Conv (s, proj, inj, t), VConv (s', v) when s = s' ->
12181218 inj (devariantize e t v)
1219- | Sum ops, VSum (tag, a) -> begin
1220- try
1219+ | Sum ops, VSum (tag, a) ->
1220+ begin try
12211221 match List.assoc tag ops.sum_cases, a with
12221222 | TCarg (sel, t), Some a -> ops.sum_inj (sel, devariantize e t a)
12231223 | TCnoarg sel, None -> ops.sum_inj (sel, Noarg)
@@ -1560,8 +1560,8 @@ let rec sameNat : type a b. a nat -> b nat -> (a, b) equal option =
15601560 fun a b ->
15611561 match a, b with
15621562 | NZ, NZ -> Some Eq
1563- | NS a', NS b' -> begin
1564- match sameNat a' b' with
1563+ | NS a', NS b' ->
1564+ begin match sameNat a' b' with
15651565 | Some Eq -> Some Eq
15661566 | None -> None
15671567 end
@@ -1756,13 +1756,13 @@ let rec del : type n. int -> n avl -> n avl_del =
17561756 | Node (bal, l, x, r) ->
17571757 if x = y then begin
17581758 match r with
1759- | Leaf -> begin
1760- match bal with
1759+ | Leaf ->
1760+ begin match bal with
17611761 | Same -> Ddecr (Eq, l)
17621762 | More -> Ddecr (Eq, l)
17631763 end
1764- | Node _ -> begin
1765- match bal, del_min r with
1764+ | Node _ ->
1765+ begin match bal, del_min r with
17661766 | _, (z, Inr r) -> Dsame (Node (bal, l, z, r))
17671767 | Same, (z, Inl r) -> Dsame (Node (More, l, z, r))
17681768 | Less, (z, Inl r) -> Ddecr (Eq, Node (Same, l, z, r))
@@ -1775,8 +1775,8 @@ let rec del : type n. int -> n avl -> n avl_del =
17751775 else if y < x then begin
17761776 match del y l with
17771777 | Dsame l -> Dsame (Node (bal, l, x, r))
1778- | Ddecr (Eq, l) -> begin
1779- match bal with
1778+ | Ddecr (Eq, l) ->
1779+ begin match bal with
17801780 | Same -> Dsame (Node (Less, l, x, r))
17811781 | More -> Ddecr (Eq, Node (Same, l, x, r))
17821782 | Less ->
@@ -1788,8 +1788,8 @@ let rec del : type n. int -> n avl -> n avl_del =
17881788 else begin
17891789 match del y r with
17901790 | Dsame r -> Dsame (Node (bal, l, x, r))
1791- | Ddecr (Eq, r) -> begin
1792- match bal with
1791+ | Ddecr (Eq, r) ->
1792+ begin match bal with
17931793 | Same -> Dsame (Node (More, l, x, r))
17941794 | Less -> Ddecr (Eq, Node (Same, l, x, r))
17951795 | More ->
@@ -1916,16 +1916,16 @@ let rec rep_equal : type a b. a rep -> b rep -> (a, b) equal option =
19161916 match ra, rb with
19171917 | Rint, Rint -> Some Eq
19181918 | Rbool, Rbool -> Some Eq
1919- | Rpair (a1, a2), Rpair (b1, b2) -> begin
1920- match rep_equal a1 b1 with
1919+ | Rpair (a1, a2), Rpair (b1, b2) ->
1920+ begin match rep_equal a1 b1 with
19211921 | None -> None
19221922 | Some Eq ->
19231923 match rep_equal a2 b2 with
19241924 | None -> None
19251925 | Some Eq -> Some Eq
19261926 end
1927- | Rfun (a1, a2), Rfun (b1, b2) -> begin
1928- match rep_equal a1 b1 with
1927+ | Rfun (a1, a2), Rfun (b1, b2) ->
1928+ begin match rep_equal a1 b1 with
19291929 | None -> None
19301930 | Some Eq ->
19311931 match rep_equal a2 b2 with
@@ -2035,8 +2035,8 @@ let rec compare : type a b. a rep -> b rep -> (string, (a, b) equal) sum =
20352035 fun a b ->
20362036 match a, b with
20372037 | I, I -> Inr Eq
2038- | Ar (x, y), Ar (s, t) -> begin
2039- match compare x s with
2038+ | Ar (x, y), Ar (s, t) ->
2039+ begin match compare x s with
20402040 | Inl _ as e -> e
20412041 | Inr Eq ->
20422042 match compare y t with
@@ -2075,23 +2075,23 @@ let rec tc : type n e. n nat -> e ctx -> term -> e checked =
20752075 fun n ctx t ->
20762076 match t with
20772077 | V s -> lookup s ctx
2078- | Ap (f, x) -> begin
2079- match tc n ctx f with
2078+ | Ap (f, x) ->
2079+ begin match tc n ctx f with
20802080 | Cerror _ as e -> e
20812081 | Cok (f', ft) ->
20822082 match tc n ctx x with
20832083 | Cerror _ as e -> e
20842084 | Cok (x', xt) ->
20852085 match ft with
2086- | Ar (a, b) -> begin
2087- match compare a xt with
2086+ | Ar (a, b) ->
2087+ begin match compare a xt with
20882088 | Inl s -> Cerror s
20892089 | Inr Eq -> Cok (App (f', x'), b)
20902090 end
20912091 | _ -> Cerror "Non fun in Ap"
20922092 end
2093- | Ab (s, t, body) -> begin
2094- match tc (NS n) (Ccons (n, s, t, ctx)) body with
2093+ | Ab (s, t, body) ->
2094+ begin match tc (NS n) (Ccons (n, s, t, ctx)) body with
20952095 | Cerror _ as e -> e
20962096 | Cok (body', et) -> Cok (Abs (n, body'), Ar (t, et))
20972097 end
@@ -2182,8 +2182,8 @@ let rec rule : type a b.
21822182 (pval, closed, (a, b) tarr) lam -> (pval, closed, a) lam -> b rlam =
21832183 fun v1 v2 ->
21842184 match v1, v2 with
2185- | Lam (x, body), v -> begin
2186- match subst body (Bind (x, v, Id)) with
2185+ | Lam (x, body), v ->
2186+ begin match subst body (Bind (x, v, Id)) with
21872187 | Ex term ->
21882188 match mode term with
21892189 | Pexp -> Inl term
@@ -2195,13 +2195,13 @@ let rec onestep : type m t. (m, closed, t) lam -> t rlam = function
21952195 | Const (r, v) -> Inr (Const (r, v))
21962196 | App (e1, e2) ->
21972197 match mode e1, mode e2 with
2198- | Pexp, _ -> begin
2199- match onestep e1 with
2198+ | Pexp, _ ->
2199+ begin match onestep e1 with
22002200 | Inl e -> Inl (App (e, e2))
22012201 | Inr v -> Inl (App (v, e2))
22022202 end
2203- | Pval, Pexp -> begin
2204- match onestep e2 with
2203+ | Pval, Pexp ->
2204+ begin match onestep e2 with
22052205 | Inl e -> Inl (App (e1, e))
22062206 | Inr v -> Inl (App (e1, v))
22072207 end
0 commit comments