[Why3-club] Problem with module translation to Coq

Guillaume Melquiond guillaume.melquiond at inria.fr
Tue Mar 4 16:40:05 CET 2014


On 04/03/2014 14:45, Julien Thierry wrote:
> Hi,
>
> When cloning a module and instantiating it's functions with two
> functions having the same name but from different modules, in the code
> generated by the Coq driver the names of the Why3 modules are lost and
> only one of the definitions is kept.

Good catch.

Your interpretation is wrong though. The issue does not have anything 
with the instantiations of several modules. It simply comes from a 
broken driver for Coq. Since the driver contains a syntax for 
"bool.Bool.orb", the Coq printer does not output the symbol, which is 
the expected behavior. While doing so, the driver also makes the 
(incorrect) assumption that no one would ever call a symbol "orb". 
Unfortunately, you just did.

I will modify the driver to remove this assumption.

Best regards,

Guillaume

PS: And in case you wonder, you would have hit the same issue by naming 
the symbol "andb", "exp", "cons", and so on.



More information about the Why3-club mailing list