let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
let new_subst =
subst_entry_j :: List.map
let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
let new_subst =
subst_entry_j :: List.map
in
let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
metasenv, new_subst, j, diff
in
let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
metasenv, new_subst, j, diff
pp (lazy ("BBB: dopo metasenv\n" ^ NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
List.map
pp (lazy ("BBB: dopo metasenv\n" ^ NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
List.map
metasenv,
subst_entry :: subst, j, diff
with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
metasenv,
subst_entry :: subst, j, diff
with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
- (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
+ (i,([],c,t,ty)) :: List.filter (fun (j,_) -> i <> j) subst
in
aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
with NCicUtils.Subst_not_found _ ->
in
aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
with NCicUtils.Subst_not_found _ ->
| NCic.Implicit (`Typeof _) ->
let mk_meta context kind =
let metasenv, _, ty, _ = mk_meta metasenv context kind in
| NCic.Implicit (`Typeof _) ->
let mk_meta context kind =
let metasenv, _, ty, _ = mk_meta metasenv context kind in
- (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
+ (n, (attrs, cc, ty)) :: List.filter (fun (x,_) -> x <> n) metasenv, ty