λ-box pretty-printer giving incorrect names in mutual fixpoint

[simon-dima]

The displayed output of

Require Import MetaCoq.ErasurePlugin.Loader.

Fixpoint
  even n := match n with O => true | S n => odd n end
with
  odd n := match n with O => false | S n => even n end
.
MetaCoq Erase even.

is

Environment: 
Inductive nat(0 parameters,computational, elimination into any sort) := 
| O 0 arguments
| S 1 arguments
Inductive bool(0 parameters,computational, elimination into any sort) := 
| true 0 arguments
| false 0 arguments
Definition Example.test_erasure.even := fun n => (let fix even { struct 0 } := 
fun n0 => match n0 with 
O => true
 | S n  => even n
end

 with odd { struct 0 } := 
fun n0 => match n0 with 
O => false
 | S n  => odd n
end

 in even) n
Program: Example.test_erasure.even

Notice how the recursive calls in even resp. odd are to the wrong function.

I am using MetaCoq 1.3.3+8.19, but the file erasure/theories/EPretty.v does not seem to have been changed much recently, so I assume this problem is also present in MetaRocq 1.4+9.0.

This may also apply to the PCUIC and Template-Rocq pretty-printers, I'm unsure how to test whether this is the case.

[4ever2]

Looks like there is a List.rev missing in

metarocq/erasure/theories/EPretty.v

Line 84 in c024752

let ctx' := List.map (fun d => {| decl_name := dname d; decl_body := None |}) defs in

The Template-Rocq pretty-printer doesn't have this problem.