-(*** delifting ***)
-
-val delift :
- int -> Cic.substitution -> Cic.context -> Cic.metasenv ->
- (Cic.term option) list -> Cic.term ->
- Cic.term * Cic.metasenv * Cic.substitution
-val restrict :
- Cic.substitution -> (int * int) list -> Cic.metasenv ->
- Cic.metasenv * Cic.substitution
-
-(** delifts the Rels in t of n
- * @raise DeliftingARelWouldCaptureAFreeVariable
+(* the delift function takes in input a metavariable index, a local_context
+ * and a term t, and substitutes every subterm t' of t with its position
+ * (searched up-to unification) in
+ * the local_context (which is the Rel moved to the canonical context).
+ * Typically, the list of optional terms is the explicit
+ * substitution that is applied to a metavariable occurrence and the result of
+ * the delift function is a term the implicit variable can be substituted with
+ * to make the term [t] unifiable with the metavariable occurrence. In general,
+ * the problem is undecidable if we consider equivalence in place of alpha
+ * convertibility. Our implementation, though, is even weaker than alpha
+ * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
+ * (missing all the other cases). Does this matter in practice?
+ * The metavariable index is the index of the metavariable that must not occur
+ * in the term (for occur check).