lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
| CoercGraph.NotMetaClosed ->
raise (Uncertain (lazy "Coercions on meta"))
| CoercGraph.SomeCoercion c ->
| CoercGraph.NotMetaClosed ->
raise (Uncertain (lazy "Coercions on meta"))
| CoercGraph.SomeCoercion c ->