diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 11:48:34 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 11:48:34 +0100 |
| commit | 4edc539b83bddb2483b9c8ba1cf82fc81c717abd (patch) | |
| tree | ac6109af8e2e634ac98608ae159e1c976e57f318 | |
| parent | ff9b5494cb1943339543eeac41683a8ec2dda437 (diff) | |
| download | smtcoq-4edc539b83bddb2483b9c8ba1cf82fc81c717abd.tar.gz smtcoq-4edc539b83bddb2483b9c8ba1cf82fc81c717abd.zip | |
Corrected a bug in the initialization of arrays for the standard version (the last element is the default)
| -rw-r--r-- | src/versions/standard/structures.ml | 9 |
1 files changed, 7 insertions, 2 deletions
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 *) |