(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
-type substitution = (int * (Cic.context * Cic.term)) list
+type substitution = (int * (Cic.context * Cic.term)) list
(** @raise SubstNotFound *)
val lookup_subst: int -> substitution -> Cic.context * Cic.term
int -> substitution -> Cic.context -> Cic.metasenv ->
(Cic.term option) list -> Cic.term ->
Cic.term * Cic.metasenv * substitution
-
+val restrict :
+ substitution -> (int * int) list -> Cic.metasenv ->
+ Cic.metasenv * substitution
(** {2 Pretty printers} *)
+val ppsubst_unfolded: substitution -> string
val ppsubst: substitution -> string
val ppterm: substitution -> Cic.term -> string
val ppcontext: ?sep: string -> substitution -> Cic.context -> string
val reset_counters: unit -> unit
*)
+(* val clean_up_meta :
+ substitution -> Cic.metasenv -> Cic.term -> Cic.term
+*)