(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
int -> substitution -> Cic.context -> Cic.metasenv ->
(Cic.term option) list -> Cic.term ->
Cic.term * Cic.metasenv * substitution
int -> substitution -> Cic.context -> Cic.metasenv ->
(Cic.term option) list -> Cic.term ->
Cic.term * Cic.metasenv * substitution
val ppsubst: substitution -> string
val ppterm: substitution -> Cic.term -> string
val ppcontext: ?sep: string -> substitution -> Cic.context -> string
val ppsubst: substitution -> string
val ppterm: substitution -> Cic.term -> string
val ppcontext: ?sep: string -> substitution -> Cic.context -> string