diff options
Diffstat (limited to 'src/common/IntegerExtra.v')
| -rw-r--r-- | src/common/IntegerExtra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index fe7d94f..c9b5dbd 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -5,7 +5,7 @@ Require Import ZBinary. From bbv Require Import ZLib. From compcert Require Import Integers Coqlib. -Require Import Coquplib. +Require Import Vericertlib. Local Open Scope Z_scope. |