| C.Var (uri,exp_named_subst) ->
let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
C.Var (uri,exp_named_subst')
- | C.Meta _
+ | C.Meta (i,l) ->
+ let l' =
+ List.map (function None -> None | Some t -> Some (aux n t)) l
+ in
+ C.Meta (i, l')
| C.Sort _
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
in
let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
let (newproof, newmetasenv''') =
- let subst_in = CicMetaSubst.apply_subst ((metano,bo')::subst) in
+ let subst_in =
+ CicMetaSubst.apply_subst ((metano,(context, bo'))::subst)
+ in
subst_meta_and_metasenv_in_proof
proof metano subst_in newmetasenv''
in
C.Appl (eliminator_ref :: make_tl term (args_no - 1))
in
let metasenv', term_to_refine' =
- CicMkImplicit.expand_implicits metasenv context term_to_refine in
+ CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
let refined_term,_,metasenv'' =
CicRefine.type_of_aux' metasenv' context term_to_refine'
in