-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
-(* performs as (apply_subst subst t) until it finds an application of *)
-(* (META [mtr]) that, once unwinding is performed, creates a new *)
-(* beta-redex; in this case up to [reductions_no] consecutive *)
-(* beta-reductions are performed. *)
-(* Hint: this function is usually called when [reductions_no] *)
-(* eta-expansions have been performed and the head of the new *)
-(* application has been unified with (META [meta_to_reduce]): *)
-(* during the unwinding the eta-expansions are undone. *)
-(* [subst] must be already unwinded *)
-val apply_subst_reducing :
- (int * int) option -> substitution -> Cic.term -> Cic.term
+val apply_subst : Cic.substitution -> Cic.term -> Cic.term
+val apply_subst_context : Cic.substitution -> Cic.context -> Cic.context
+val apply_subst_metasenv: Cic.substitution -> Cic.metasenv -> Cic.metasenv
+
+(*** delifting ***)