diff options
Diffstat (limited to 'src/Compilers/Z/Syntax.v')
| -rw-r--r-- | src/Compilers/Z/Syntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v index de4626adb..dbc739dcb 100644 --- a/src/Compilers/Z/Syntax.v +++ b/src/Compilers/Z/Syntax.v @@ -1,6 +1,6 @@ (** * PHOAS Syntax for expression trees on ℤ *) Require Import Coq.ZArith.ZArith. -Require Import Bedrock.Word. +Require Import bbv.WordScope. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.TypeUtil. |