[Why3-club] Problem with module translation to Coq
guillaume.melquiond at inria.fr
Tue Mar 4 16:40:05 CET 2014
On 04/03/2014 14:45, Julien Thierry wrote:
> 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.
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.
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