- 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
GrafiteDisambiguate.disambiguate_nterm
status None ctx [] [] ("",0,src) in
let src = NCicUntrusted.apply_subst status subst [] src in
- 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
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 =
let fresh_uri status prefix suffix =
let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
let rec diverge u i =
-let basic_index_ncoercion (name,t,s,d,position,arity) status =
+let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status =
-let basic_eval_ncoercion (name,t,s,d,p,a) status =
+let basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
in
let status = NCicCoercion.index_coercion status name t s d a p in
NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
in
let status = NCicCoercion.index_coercion status name t s d a p in
List.fold_left
(fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
List.fold_left
(fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
- let info = name,t,s,d,p,a in
+ let info = name,compose,t,s,d,p,a in
let st = NCicLibrary.add_obj st obj in
let st = basic_index_ncoercion info st in
uri::uris, info::infos, st)
let st = NCicLibrary.add_obj st obj in
let st = basic_index_ncoercion info st in
uri::uris, info::infos, st)
- let aux (name,t,s,d,p,a) ~refresh_uri_in_term =
+ let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term =
let t = refresh_uri_in_term t in
let s = refresh_uri_in_term s in
let d = refresh_uri_in_term d in
let t = refresh_uri_in_term t in
let s = refresh_uri_in_term s in
let d = refresh_uri_in_term d in
- basic_index_ncoercion (name,t,s,d,p,a)
+ basic_index_ncoercion (name,compose,t,s,d,p,a)
in
let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
~refresh_uri_in_reference ~alias_only status
=
if not alias_only then
in
let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
~refresh_uri_in_reference ~alias_only status
=
if not alias_only then
- status (name,t,cpos,arity)
+ status (name,compose,t,cpos,arity)
=
let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
let status, uris =
=
let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
let status, uris =
- basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+ basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
-let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
- let newast_ty,metasenv,subst,status,ty =
+let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt =
+ let metasenv,subst,status,ty =
GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst status subst [] ty in
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
let status, src, tgt, cpos, arity =
src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
let status, uris =
GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
let status, src, tgt, cpos, arity =
src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
let status, uris =
- basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+ basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status