[Why3-club] Problem with module translation to Coq

Julien Thierry thierry at adacore.com
Tue Mar 4 14:45:05 CET 2014


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.

I'm joining a file where this problem causes a typing error in the 
axiom Array_Generic_Op_Axiom.op_def due to the different signatures
of Array.orb and Array_Generic_Op_Axiom.orb. In the end, only Array.orb
is defined in the Coq code.

Regards,

-- 
Julien Thierry
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.mlw
Type: text/x-java
Size: 1396 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140304/a0c381be/attachment.java>


More information about the Why3-club mailing list