- (match NCicEnvironment.sup u with
- | None -> raise (fail_exc metasenv subst context meta t)
- | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
+ if swap then
+ match NCicEnvironment.sup u with
+ | None -> raise (fail_exc metasenv subst context meta t)
+ | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
+ else
+ NCic.Sort (NCic.Type (
+ match NCicEnvironment.sup NCicEnvironment.type0 with
+ | Some x -> x
+ | _ -> assert false))