(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
let src = NCicUntrusted.apply_subst subst [] src in
(* CHECK that the declared pattern matches the abstraction *)
let _ = NCicUnification.unify status metasenv subst ctx ty src in
let src = NCicUntrusted.apply_subst subst [] src in
(* CHECK that the declared pattern matches the abstraction *)
let _ = NCicUnification.unify status metasenv subst ctx ty src in
let status, tgt, arity =
let metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
let status, tgt, arity =
let metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
let tgt = NCicUntrusted.apply_subst subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
let tgt = NCicUntrusted.apply_subst subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
let metasenv,subst,status,ty =
let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
let metasenv,subst,status,ty =
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst subst [] ty in
let metasenv,subst,status,t =
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst subst [] ty in
let metasenv,subst,status,t =
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst subst [] t in
let status, src, tgt, cpos, arity =
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst subst [] t in
let status, src, tgt, cpos, arity =