| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, compose, None) ->
let status, t, ty, source, target =
let o_t = NotationPt.Ident (name,None) in
let metasenv,subst, status,t =
GrafiteDisambiguate.disambiguate_nterm
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, compose, None) ->
let status, t, ty, source, target =
let o_t = NotationPt.Ident (name,None) in
let metasenv,subst, status,t =
GrafiteDisambiguate.disambiguate_nterm