Merge pull request #76 from coq-community/mc1343

Adapt to math-comp/math-comp#1343
coq-community · Feb 14, 2025 · a8fea35 · a8fea35
2 parents 5c83ad4 + 4eedf6d
commit a8fea35
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/theories/dfa.v b/theories/dfa.v
@@ -1,5 +1,6 @@
 (* Authors: Christian Doczkal and Jan-Oliver Kaiser *)
 (* Distributed under the terms of CeCILL-B. *)
+From Coq Require Import Setoid.
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages.
 

diff --git a/theories/setoid_leq.v b/theories/setoid_leq.v
@@ -1,7 +1,7 @@
 (* Author: Christian Doczkal  *)
 (* Distributed under the terms of CeCILL-B. *)
 
-From Coq Require Import Basics Setoid Morphisms.
+From Coq Require Import Basics Setoid Morphisms BinPos.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 
 Set Implicit Arguments.