exception Free
exception OccurCheck
+val delift :
+ Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
+
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
type substitution = (int * Cic.term) list
(* Only the metavariables declared in [metasenv] *)
(* can be used in [t1] and [t2]. *)
val fo_unif :
- (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term -> substitution
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ substitution * Cic.metasenv
(* apply_subst subst t *)
(* applies the substitution [sust] to [t] *)