[Why3-club] Problem with module translation to Coq

Julien Thierry 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
> end
> 
> module C
>   use import bool.Bool
>   clone B with function op = orb
>   goal g: false
> end
> 
> 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

-- 
Julien Thierry




More information about the Why3-club mailing list