-
-(* the delift function takes in input an ordered list of optional terms *)
-(* [t1,...,tn] and a term t, and substitutes every tk = Some (rel(nk)) with *)
-(* rel(k). 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 delift function takes in input a metavariable index, an ordered list of
+ * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
+ * (rel(nk)) with rel(k). 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).
+ *)