diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 19:34:19 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 19:34:19 +0100 |
| commit | 7c57fa0cc7a24be11875607e2a2fc9bba98ad2e0 (patch) | |
| tree | db8fdd9c0f9be522545f0b1ca00289d81a20187a | |
| parent | e191cc298e684fa4231c97abf4f89ab0f1b3a42c (diff) | |
| download | smtcoq-7c57fa0cc7a24be11875607e2a2fc9bba98ad2e0.tar.gz smtcoq-7c57fa0cc7a24be11875607e2a2fc9bba98ad2e0.zip | |
COrrect implementation of foldi_cont and foldi_down_cont
| -rw-r--r-- | src/versions/standard/Int63/Int63Native_standard.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v index 6224e34..c8eadfd 100644 --- a/src/versions/standard/Int63/Int63Native_standard.v +++ b/src/versions/standard/Int63/Int63Native_standard.v @@ -170,9 +170,9 @@ Definition foldi_cont cont else let (_,r) := iter_int31 (to - from) _ (fun (jy: (int * (A -> B))%type) => - let (j,y) := jy in ((j+1)%int, f j y) - ) (from, cont) in - f to r. + let (j,y) := jy in ((j-1)%int, f j y) + ) (to, cont) in + f from r. Definition foldi_down_cont {A B : Type} @@ -183,9 +183,9 @@ Definition foldi_down_cont cont else let (_,r) := iter_int31 (from - downto) _ (fun (jy: (int * (A -> B))%type) => - let (j,y) := jy in ((j-1)%int, f j y) - ) (from, cont) in - f downto r. + let (j,y) := jy in ((j+1)%int, f j y) + ) (downto, cont) in + f from r. (* Fake print *) |