| _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
"Prod: the type %s of the source of %s is not a sort"
(status#ppterm ~subst ~metasenv ~context sort)
| _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
"Prod: the type %s of the source of %s is not a sort"
(status#ppterm ~subst ~metasenv ~context sort)