[Why3-club] Problem with module translation to Coq
thierry at adacore.com
Tue Mar 4 14:45:05 CET 2014
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 1396 bytes
Desc: not available
More information about the Why3-club