aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-09-30 12:20:00 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-09-30 12:22:45 -0400
commitb59651f1fb0128def9a696af7082fc8cc9933d17 (patch)
tree3fd7ca1325914f655f8123fd14300cc4ad0aea60 /src/Util/ListUtil.v
parent8632c54a04313371da2d4740442e9d61fd986c5a (diff)
Work around bug #5112 ([Arguments id /] broken)
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r--src/Util/ListUtil.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 4f544d2c8..749b1b09f 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -211,8 +211,8 @@ Hint Rewrite <- @firstn_cons @firstn_app @List.firstn_firstn : pull_firstn.
Hint Rewrite @firstn_all2 @removelast_firstn @firstn_removelast using omega : push_firstn.
Hint Rewrite @firstn_all2 @removelast_firstn @firstn_removelast using omega : simpl_firstn.
-Local Arguments value / .
-Local Arguments error / .
+Local Arguments value / _ _.
+Local Arguments error / _.
Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l).