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
with
| NCicUnification.UnificationFailure _
| NCicUnification.Uncertain _
- | MultiPassDisambiguator.DisambiguationError _ ->
+ | GrafiteDisambiguate.Error _ ->
raise (GrafiteTypes.Command_error "bad source pattern"))
| _ -> assert false
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 fresh_uri status prefix suffix =
let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
let rec diverge u i =
- if NCicLibrary.aliases_of u = [] then u
+ if NCicLibrary.aliases_of status u = [] then u
else diverge (mk ("__" ^ string_of_int i)) (i+1)
in
diverge (mk "") 0
~refresh_uri_in_reference ~alias_only status
=
if not alias_only then
- List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+ List.fold_right
+ (aux ~refresh_uri_in_term:(refresh_uri_in_term
+ (status:>NCicEnvironment.status))) l status
else
status
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