Only export R from Rbase to avoid name clashes

In particular, there's a constructor called IRQ.
rems-project · Nov 14, 2023 · fa0c524 · fa0c524
1 parent c20045e
commit fa0c524
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/Real.v b/src/Real.v
@@ -65,13 +65,15 @@
 (*  SUCH DAMAGE.                                                            *)
 (*==========================================================================*)
 
-Require Export Rbase.
+Require Import Rbase.
 Require Import Reals.
 Require Export ROrderedType.
 Require Import Sail.Values.
 Require Import Lia.
 Local Open Scope Z.
 
+Export Rdefinitions(R).
+
 (* "Decidable" in a classical sense... *)
 #[export] Instance Decidable_eq_real : forall (x y : R), Decidable (x = y) :=
   Decidable_eq_from_dec Req_dec.