From 4edc539b83bddb2483b9c8ba1cf82fc81c717abd Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 11 Feb 2015 11:48:34 +0100 Subject: Corrected a bug in the initialization of arrays for the standard version (the last element is the default) --- src/versions/standard/structures.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/versions/standard/structures.ml') diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index ae3157b..a5fd69b 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -52,10 +52,15 @@ let cset = gen_constant parray_modules "set" let max_array_size : int = 4194302 let mkArray : Term.types * Term.constr array -> Term.constr = fun (ty, a) -> + let l = (Array.length a) - 1 in snd (Array.fold_left (fun (i,acc) c -> - let acc' = mklApp cset [|ty; acc; mkInt i; c|] in + let acc' = + if i = l then + acc + else + mklApp cset [|ty; acc; mkInt i; c|] in (i+1,acc') - ) (0,mklApp cmake [|ty; mkInt (Array.length a); a.(0)|]) a) + ) (0,mklApp cmake [|ty; mkInt l; a.(l)|]) a) (* Differences between the two versions of Coq *) -- cgit