aboutsummaryrefslogtreecommitdiffstats
path: root/src/common
diff options
context:
space:
mode:
Diffstat (limited to 'src/common')
-rw-r--r--src/common/NonEmpty.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v
index 31adbda..5764208 100644
--- a/src/common/NonEmpty.v
+++ b/src/common/NonEmpty.v
@@ -125,5 +125,5 @@ Fixpoint fold_left {A B} (f: A -> B -> A) (l: non_empty B) (a: A) {struct l} : A
Fixpoint fold_right {A B} (f: B -> A -> A) (a: A) (l: non_empty B) {struct l} : A :=
match l with
| singleton a' => f a' a
- | b ::| t => fold_right f (f b a) t
+ | b ::| t => f b (fold_right f a t)
end.