Compatibility with Analysis master

math-comp · Nov 3, 2021 · d68bdf6 · d68bdf6
1 parent 88299b0
commit d68bdf6
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/complete_dioid.v b/complete_dioid.v
@@ -1,6 +1,7 @@
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice order.
 From mathcomp Require Import fintype ssrnat bigop.
+Require Import mathcomp.analysis.boolp.
 Require Import mathcomp.analysis.classical_sets.
 Require Import HB_wrappers dioid complete_lattice.