From 3eb1a83c1362c0eae2110444935bcbe2114dd763 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 14 Feb 2022 18:02:12 +0900 Subject: [PATCH] fix compilation with Coq 8.15 --- ecc_modern/ldpc_algo.v | 2 +- ecc_modern/ldpc_algo_proof.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v index 58d38438..910319ad 100644 --- 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 index 1a57896a..9dfd8cd8 100644 --- 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.