Bug when trying to use a lemma from a section with clones

[guilhemmizrahi-jpg]

Context

I have an abstract theory in which I clone import PolyArray.
In another file I have a section that clones this abstract theory and use it inside a lemma.

Bug

In a third file, when I try to use rewrite lemma, I reach the following error:

anomaly: File "src/ecCoreSubst.ml", line 733, characters 4-10: Assertion failed

The example for the bug is fairly large so I have not included it here but can provide more info as necessary.

[oskgo]

Can you try minimizing the example? Bugs not related to performance tend to have fairly short minimal reproductions.

You can also get a full backtrace using OCAMLRUNPARAM=b easycrypt <path to easycrypt file>.