function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (_,C.Def (_,Some _)))::_ -> assert false
in
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
(* Checks suppressed *)
- CicSubstitution.lift_meta l ty
+ CicSubstitution.subst_meta l ty
| C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
C.Sort (C.Type (CicUniv.fresh()))
| C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)