adapt to coq/coq#17281

mit-plv · Feb 22, 2023 · 93f79b6 · 93f79b6
1 parent 48f5b60
commit 93f79b6
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 1 deletion.
diff --git a/src/Arithmetic/SolinasReduction.v b/src/Arithmetic/SolinasReduction.v
@@ -10,7 +10,7 @@ Require Import Crypto.Arithmetic.ModOps.
 Require Import Crypto.Arithmetic.Partition.
 Require Import Crypto.Arithmetic.UniformWeight.
 Require Import Crypto.Arithmetic.Saturated.
-Require Coq.btauto.Btauto.
+Require Import (*hints*) Coq.btauto.Algebra.
 Require Coq.Structures.OrdersEx.
 Require Import Crypto.Util.ListUtil.StdlibCompat.
 Require Import Crypto.Util.ZUtil.ModInv.

diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia.
+Require Import (*hints*) Coq.btauto.Algebra.
 Require Import bedrock2.Syntax.
 Require Import coqutil.Word.Interface coqutil.Word.Properties.
 Require Import coqutil.Map.Interface.

diff --git a/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v b/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia.
+Require Import (*hints*) Coq.btauto.Algebra.
 Require Import bedrock2.Syntax.
 Require Import coqutil.Word.Interface coqutil.Word.Properties.
 Require Import coqutil.Map.Interface.