The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

> A good idea is generally not to store the constants directly as an
> argument of the constructor. It is better to store them in a map and use
> an index in the constructor. There are two advantages. First, you no
> longer care about it being evaluated. Second, your simplification code
> can now be made aware that two constants are equal.

Thanks, that sounds like a better idea indeed. Could you detail a bit
more how it would work, though? The interpretation function would still
have to take this map as argument, if I'm not mistaking? How do you
prevent the map itself (and the constants inside) from being evaluated?

> Still, you might later on still have some evaluation issues, especially
> when inverting the reification process. In that case, I suggest taking a
> look at the "Strategy" vernacular.

Thanks again, I didn't know about that one; I will keep that in mind.