I hope the assertion will never be reached, but I ignore why.
I think this is really a bug and code must be written there.
| x::_ -> x
| _ -> assert false))
| `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
| x::_ -> x
| _ -> assert false))
| `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
+ | `XTInd -> assert false(*CSC: was not handled, OCaml 4.0 complains. ??? *)
in
pp(lazy("try_coercion " ^
status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
in
pp(lazy("try_coercion " ^
status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^