- | _, B.Sort _ -> error1 err "not a function type" m u
- | mu, B.Bind (_, B.Abst u, _) ->
+ | _, B.Sort _ ->
+ error1 err "not a function type" m u
+ | mu, B.Bind (_, B.Abst (_, u), _) ->
let h = H.apply h in f x (B.Sort (a, h))
| B.LRef (_, i) ->
begin match BR.get m i with
let h = H.apply h in f x (B.Sort (a, h))
| B.LRef (_, i) ->
begin match BR.get m i with
f x (BS.lift (succ i) (0) w)
| B.Abbr (B.Cast (_, w, _)) ->
f x (BS.lift (succ i) (0) w)
f x (BS.lift (succ i) (0) w)
| B.Abbr (B.Cast (_, w, _)) ->
f x (BS.lift (succ i) (0) w)
| _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
| _, _, E.Abbr _ -> assert false
| _, _, E.Void ->
| _, _, E.Abbr (B.Cast (_, w, _)) -> f x w
| _, _, E.Abbr _ -> assert false
| _, _, E.Void ->