- type_of f g c u
- | B.Bind (id, B.Abst u, t) ->
- let f tt = f (B.Bind (id, B.Abst u, tt)) in
- let f cc = type_of f g cc t in
- let f _ = R.push f c (B.Abst u) in
- type_of f g c u
- | B.Bind (id, B.Void, t) ->
- let f tt = f (B.Bind (id, B.Void, tt)) in
- let f cc = type_of f g cc t in
- R.push f c B.Void
- | B.Appl (v, t) ->
- let f tt cc = function
- | R.Sort _ -> error1 "not a function" c t
- | R.Abst w ->
- let f b =
- if b then f (B.Appl (v, tt)) else
- error2 "the term" c v "must be of type" cc w
- in
- type_of (are_convertible f cc w) g c v
+ type_of err f ~si g m v
+ | B.Bind (B.Abst (a, u), t) ->
+ let f xu xt tt =
+ f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)