From d68bdf6dafee20555e99b38b1e2f07a5ddc752f3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 3 Nov 2021 14:00:18 +0100 Subject: [PATCH] Compatibility with Analysis master --- complete_dioid.v | 1 + 1 file changed, 1 insertion(+) diff --git a/complete_dioid.v b/complete_dioid.v index af5ae77..fd6c252 100644 --- 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.