-
Jean-Christophe Filliâtre authored
instead of a function of type int->'a a coercion is declared from arrays to sequences, so that notation a[i] in the logic now refers to the sequence operation small caveat: you have to open module seq.Seq to be able to use this notation
4898a45d