| None -> assert false
;;
-let pos_of x t =
- match t with
- | NCic.Appl l -> pos_in_list x l
- | _ -> assert false
-;;
-
let rec count_prod = function
| NCic.Prod (_,_,x) -> 1 + count_prod x
| _ -> 0
(metasenv,[]) upl
in
let bo = NCicUntrusted.apply_subst subst [] bo in
+ let p = NCicUntrusted.apply_subst subst [] p in
+ let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
let metasenv = toposort metasenv in
let bo = close_in_context bo metasenv in
let pos =
match p with
| NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
- | _ -> assert false
+ | t -> assert false
in
let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity 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
in
- NRstatus.Serializer.register "ncoercion" aux_l
+ NCicLibrary.Serializer.register#run "ncoercion"
+ object(self : 'a NCicLibrary.register_type)
+ method run = aux_l
+ end
;;
let basic_eval_and_record_ncoercion infos status =