diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-30 12:20:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-30 12:22:45 -0400 |
| commit | b59651f1fb0128def9a696af7082fc8cc9933d17 (patch) | |
| tree | 3fd7ca1325914f655f8123fd14300cc4ad0aea60 /src | |
| parent | 8632c54a04313371da2d4740442e9d61fd986c5a (diff) | |
Work around bug #5112 ([Arguments id /] broken)
Diffstat (limited to 'src')
| -rw-r--r-- | src/BoundedArithmetic/Interface.v | 4 | ||||
| -rw-r--r-- | src/Util/ListUtil.v | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/BoundedArithmetic/Interface.v b/src/BoundedArithmetic/Interface.v index 152c43cee..932d88ac9 100644 --- a/src/BoundedArithmetic/Interface.v +++ b/src/BoundedArithmetic/Interface.v @@ -20,14 +20,14 @@ Class bounded_in_range_cls (x y z : Z) := is_bounded_in_range : x <= y < z. Ltac bounded_solver_tac := solve [ eassumption | typeclasses eauto | omega ]. Hint Extern 0 (bounded_in_range_cls _ _ _) => unfold bounded_in_range_cls; bounded_solver_tac : typeclass_instances. -Global Arguments bounded_in_range_cls / . +Global Arguments bounded_in_range_cls / _ _ _. Global Instance decode_range_bound {n W} {decode : decoder n W} {H : is_decode decode} : forall x, bounded_in_range_cls 0 (decode x) (2^n) := H. Class bounded_le_cls (x y : Z) := is_bounded_le : x <= y. Hint Extern 0 (bounded_le_cls _ _) => unfold bounded_le_cls; bounded_solver_tac : typeclass_instances. -Global Arguments bounded_le_cls / . +Global Arguments bounded_le_cls / _ _. Inductive bounded_decode_pusher_tag := decode_tag. 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). |