-val apply_subst : substitution -> Cic.term -> Cic.term
-
-(* 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_context : substitution -> Cic.context -> Cic.context
-val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
-
-(** {2 Pretty printers} *)
-
-val ppsubst: substitution -> string
-val ppterm: substitution -> Cic.term -> string
-val ppcontext: ?sep: string -> substitution -> Cic.context -> string
-val ppterm_in_context:
- substitution -> Cic.term -> (Cic.name option) list -> string
-val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string