if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
else
(try
- let newast,metasenv,subst,status,src =
+ let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
status None ctx [] [] ("",0,src) in
let src = NCicUntrusted.apply_subst status subst [] src in
aux 0 [] ty
in
let status, tgt, arity =
- let newast, metasenv,subst,status,tgt =
+ let metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
status None [] [] [] ("",0,tgt) in
let tgt = NCicUntrusted.apply_subst status subst [] tgt in
;;
let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
- let newast_ty,metasenv,subst,status,ty =
+ let metasenv,subst,status,ty =
GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst status subst [] ty in
- let newast_t,metasenv,subst,status,t =
+ let metasenv,subst,status,t =
GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in