[Why3-club] Problem with module translation to Coq
thierry at adacore.com
Tue Mar 4 17:24:11 CET 2014
On 2014-03-04 16:44, Jean-Christophe Filliatre wrote:
> Dear Julien,
> This is indeed a bug; thanks for reporting it.
> It can be simplified even further, for instance into the following:
> module B
> function orb int int : int
> function op bool bool : bool
> axiom ax: op True True = False
> module C
> use import bool.Bool
> clone B with function op = orb
> goal g: false
> The problem comes from Coq's driver, that prints "orb" for Why3's symbol
> bool.Bool.orb in any circumstance, but it is now shadowed by your own
> symbol "orb".
> A simple workaround is to add names such as "orb" appearing in Coq's
> driver to the black list at begginning of file src/printer/coq.ml. Then
> your "orb" is renamed into "orb1".
Thank you and Guillaume for the explanations and the workaround
More information about the Why3-club