+
+let delift context metasenv l t =
+ let module S = CicSubstitution in
+ let to_be_restricted = ref [] in
+ let rec deliftaux k =
+ let module C = Cic in
+ function
+ C.Rel m ->
+ if m <=k then
+ C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
+ (*CSC: deliftato la regola per il LetIn *)
+ else
+ (match List.nth context (m-k-1) with
+ Some (_,C.Def t) -> deliftaux k (S.lift m t)
+ | Some (_,C.Decl t) ->
+ (* It may augment to_be_restricted *)
+ ignore (deliftaux k (S.lift m t)) ;
+ C.Rel ((position (m-k) l) + k)
+ | None -> raise RelToHiddenHypothesis)
+ | C.Var _ as t -> t
+ | C.Meta (i, l1) as t ->
+ let rec deliftl j =
+ function
+ [] -> []
+ | None::tl -> None::(deliftl (j+1) tl)
+ | (Some t)::tl ->
+ let l1' = (deliftl (j+1) tl) in
+ try
+ Some (deliftaux k t)::l1'
+ with
+ RelToHiddenHypothesis
+ | NotInTheList ->
+ to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+ in
+ let l' = deliftl 1 l1 in
+ C.Meta(i,l')
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
+ | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
+ | C.Appl l -> C.Appl (List.map (deliftaux k) l)
+ | C.Const _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
+ C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t,
+ List.map (deliftaux k) pl)
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, i, ty, bo) ->
+ (name, i, deliftaux k ty, deliftaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, liftedfl)
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl =
+ List.map
+ (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, liftedfl)
+ in
+ let res = deliftaux 0 t in
+ res, restrict !to_be_restricted metasenv
+;;
+
+(**** END OF DELIFT ****)
+
+type substitution = (int * Cic.term) list
+