(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
- status None ctx [] [] ("",0,src) in
+ status `XTSort ctx [] [] ("",0,src) in
let src = NCicUntrusted.apply_subst status subst [] src in
(* CHECK that the declared pattern matches the abstraction *)
let _ = NCicUnification.unify status metasenv subst ctx ty src in
aux 0 [] ty
in
let status, tgt, arity =
- let metasenv,subst,status,tgt =
+ let _metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
- status None [] [] [] ("",0,tgt) in
+ status `XTSort [] [] [] ("",0,tgt) in
let tgt = NCicUntrusted.apply_subst status subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
exception Stop;;
-let close_graph name t s d to_s from_d p a status =
+let close_graph _name t s d to_s from_d _p a status =
let c =
List.find
(function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
let pos =
match p with
| NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
- | t -> raise Stop
+ | _t -> raise Stop
in
let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
let d = refresh_uri_in_term d in
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
+ let aux_l l ~refresh_uri_in_universe:_ ~refresh_uri_in_term
+ ~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
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
+ GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,ty) in
assert (metasenv=[]);
let ty = NCicUntrusted.apply_subst status subst [] ty in
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status (`XTSome ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
let t = NCicUntrusted.apply_subst status subst [] t in
let status, src, tgt, cpos, arity =