fix compilation with Coq 8.15

affeldt-aist · Feb 14, 2022 · 3eb1a83 · 3eb1a83
1 parent 1c784df
commit 3eb1a83
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v
@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-Require Import Wf Recdef Reals.
+Require Import Init.Wf Recdef Reals.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext Rbigop f2 subgraph_partition tanner.

diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v
@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-Require Import Wf_nat Wf Recdef Reals.
+Require Import Wf_nat Init.Wf Recdef Reals.
 From mathcomp Require Import all_ssreflect perm zmodp matrix ssralg.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext ssr_ext ssralg_ext bigop_ext Rbigop f2.