From 8a90b293e047d2e43e952381a6b349a6f28f1c8f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 7 Sep 2023 13:42:34 +0200 Subject: [PATCH] Don't require nsatz in exp.v This avoid having coqchk on probability.v report about axioms of the stdlib (although it still reports about all primitive int and float primitives, due to coq-elpi offering some interface to them). --- theories/exp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/exp.v b/theories/exp.v index c7316c04f..b21b553f9 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import mathcomp_extra. -Require Import reals ereal nsatz_realtype. +Require Import reals ereal. Require Import signed topology normedtype landau sequences derive realfun. Require Import itv convex.