From f221d60a05aa58cad1eb44fb53fae29333f69472 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 17 Jan 2025 13:22:34 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19801 --- theories/common.v | 2 +- theories/lra.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/common.v b/theories/common.v index 1a90818..72f9da2 100644 --- a/theories/common.v +++ b/theories/common.v @@ -1,5 +1,5 @@ From elpi Require Import elpi. -From Coq Require Import QArith. +From Coq Require Import PeanoNat BinNat Zbool QArith. From Coq.micromega Require Import OrderedRing RingMicromega. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint. From mathcomp.zify Require Import ssrZ zify. diff --git a/theories/lra.v b/theories/lra.v index ea1fade..5137091 100644 --- a/theories/lra.v +++ b/theories/lra.v @@ -1,5 +1,5 @@ From elpi Require Import elpi. -From Coq Require Import QArith Ring. +From Coq Require Import BinNat QArith Ring. From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto Lqa. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq. From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.