exception MetaSubstFailure of string
exception Uncertain of string
exception AssertFailure of string
+exception DeliftingARelWouldCaptureAFreeVariable;;
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
val restrict :
Cic.substitution -> (int * int) list -> Cic.metasenv ->
Cic.metasenv * Cic.substitution
+
+(** delifts the Rels in t of n
+ * @raise DeliftingARelWouldCaptureAFreeVariable
+ *)
+val delift_rels : int -> Cic.term -> Cic.term
+
(** {2 Pretty printers} *)
val ppsubst_unfolded: Cic.substitution -> string