(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
- None status ctx [] [] ("",0,src) in
+ status None ctx [] [] ("",0,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
- None status [] [] [] ("",0,tgt) in
+ status None [] [] [] ("",0,tgt) in
let tgt = NCicUntrusted.apply_subst subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
;;
let record_ncoercion =
- let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term =
+ let aux (name,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
basic_index_ncoercion (name,t,s,d,p,a)
in
- let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
- List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
+ let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
+ ~refresh_uri_in_reference
+ =
+ List.fold_right (aux ~refresh_uri_in_term) l
in
- NCicLibrary.Serializer.register#run "ncoercion"
- object(self : 'a NCicLibrary.register_type)
- method run = aux_l
- end
+ GrafiteTypes.Serializer.register#run "ncoercion" aux_l
;;
let basic_eval_and_record_ncoercion infos status =
let status, uris =
basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
in
- status,`New uris
+ status,uris
;;
-let eval_ncoercion status name t ty (id,src) tgt =
-
+let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
let metasenv,subst,status,ty =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+ GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst subst [] ty in
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst 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
in
- status,`New uris
+ status,uris
;;