[Why3-club] Pb. with the matrix library

2014-01-24 Thread Sandrine Blazy
Hi, I don't understand the errors I've got when I write the following module. File maze.mlw, line 5, characters 2-26: Symbol set is already defined in the current scope module Maze use import int.Int use import bool.Bool use import matrix.Matrix as M use import matrix.Syntax type

Re: [Why3-club] Pb. with the matrix library

2014-01-24 Thread Andrei Paskevich
On 24 January 2014 11:02, Sandrine Blazy sandrine.bl...@irisa.fr wrote: Hi, I don't understand the errors I've got when I write the following module. File maze.mlw, line 5, characters 2-26: Symbol set is already defined in the current scope module Maze use import int.Int use import