fix

Author: affeldt-aist

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.