Printing unification rules by using print unif_rule or verbose fails.
The problem is in Term.term_of_rhs: r.arities.(i) is invalid if i corresponds to a RHS extra variable.
Contrary to what is said in term.ml, r.arities does not provide the arities of the pattern variables bound in the RHS but those in the LHS only.
And the arity is not recorded in scope.ml in the cases M_URHS. In the case of P_Wild, one could use List.length env.
Printing unification rules by using
print unif_ruleorverbosefails. The problem is in Term.term_of_rhs: r.arities.(i) is invalid if i corresponds to a RHS extra variable. Contrary to what is said in term.ml, r.arities does not provide the arities of the pattern variables bound in the RHS but those in the LHS only. And the arity is not recorded in scope.ml in the cases M_URHS. In the case of P_Wild, one could use List.length env.