adapt to coq/coq#17281

mit-plv · Feb 22, 2023 · cb9e8bf · cb9e8bf
1 parent 7e6d138
commit cb9e8bf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v
@@ -7,7 +7,7 @@ Require Import Kami.RefinementFacts.
 
 Require Import FunctionalExtensionality.
 
-Require Btauto.
+Require Import (hints) btauto.Algebra.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.