Commit 2755001d authored by Martin Clochard's avatar Martin Clochard

Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3

Conflicts:
	examples/avl/priority_queue/why3session.xml
	examples/avl/priority_queue/why3shapes.gz
parents 1e331507 fd8ace5d
......@@ -313,15 +313,15 @@ module ToSeq
to_seq a l u = S.empty
axiom to_seq_cons:
forall a: array 'a, l u: int. l < u ->
forall a: array 'a, l u: int. 0 <= l < u <= length a ->
to_seq a l u = S.cons a[l] (to_seq a (l+1) u)
lemma to_seq_nth:
forall a: array 'a, l i u: int. l <= i < u ->
forall a: array 'a, l i u: int. 0 <= l <= i < u <= length a ->
S.get (to_seq a l u) (i - l) = a[i]
lemma to_seq_length:
forall a: array 'a, l u: int. l <= u ->
forall a: array 'a, l u: int. 0 <= l <= u <= length a ->
S.length (to_seq a l u) = u - l
val to_seq (a: array 'a) (l u: int) : S.seq 'a
......
......@@ -381,12 +381,12 @@ let load_icon_names () =
let ide = config () in
let iconset = ide.iconset in
let _,iconsets = iconsets () in
let d =
let iconset,d =
try
List.assoc iconset iconsets
iconset, List.assoc iconset iconsets
with Not_found ->
try
List.assoc "fatcow" iconsets
"fatcow", List.assoc "fatcow" iconsets
with Not_found ->
failwith "No icon set found"
in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment