- (*CSC: This code is bugged, since it does a List.map instead
- * of a List.fold, withouth calling eta_fixing with the
- * current context. Indeed, eta_fix always starts now in the
- * empty context. Instead of fixing this piece of code and
- * adding a new argument to eta_fix, I just skip eta_fixing
- * of the CurrentProof metasenv. Does this break well-typedness?