diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index 1c8468e68..9193ea17f 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -32,7 +32,7 @@ Require Import Crypto.Util.Tactics.UnfoldArg. Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.Option. -Require Import Bedrock.Word. +Require Import bbv.WordScope. (** The final tactic in this file, [do_reflective_pipeline], takes a goal of the form |