for the CI

Author: affeldt-aist

_CoqProject

@@ -29,6 +29,7 @@ classical/filter.v
 reals/constructive_ereal.v
 reals/reals.v
 reals/real_interval.v
+reals/interval_inference.v
 reals/signed.v
 reals/prodnormedzmodule.v
 reals/all_reals.v

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Coq Require Setoid.
+From Corelib Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

reals/all_reals.v

@@ -1,3 +1,4 @@
+From mathcomp Require Export interval_inference.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.
 From mathcomp Require Export real_interval.