* http://helm.cs.unibo.it/
*)
-exception MetaSubstFailure of string
-exception Uncertain of string
-exception AssertFailure of string
+exception MetaSubstFailure of string Lazy.t
+exception Uncertain of string Lazy.t
+exception AssertFailure of string Lazy.t
+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 :
+ Cic.substitution -> Cic.metasenv -> int -> Cic.term ->
+ Cic.term * Cic.substitution * Cic.metasenv
+
(** {2 Pretty printers} *)
val ppsubst_unfolded: Cic.substitution -> string
val ppsubst: Cic.substitution -> string
val ppterm: Cic.substitution -> Cic.term -> string
val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string
-val ppterm_in_context:
+val ppterm_in_name_context:
Cic.substitution -> Cic.term -> (Cic.name option) list -> string
-val ppmetasenv: ?sep: string -> Cic.metasenv -> Cic.substitution -> string
+val ppterm_in_context:
+ Cic.substitution -> Cic.term -> Cic.context -> string
+val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string
(** {2 Format-like pretty printers}
* As above with prototypes suitable for toplevel/ocamldebug printers. No