From eebc676ce4978b7e408c427889bae356d8b0efdc Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Thu, 27 Jun 2019 23:35:03 +0200
Subject: Define constructive real numbers as Cauchy sequences of rational
 numbers. Redefine classical real numbers as a quotient of those constructive
 real numbers.

---
 plugins/syntax/r_syntax.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 649b51cb0e..66db924051 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -101,10 +101,11 @@ let bigint_of_z c = match DAst.get c with
 
 let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
 let r_modpath = MPfile (make_dir rdefinitions)
+let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl")
 let r_path = make_path rdefinitions "R"
 
 let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
+let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult")
 let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
 
 let binintdef = ["Coq";"ZArith";"BinIntDef"]
-- 
cgit v1.2.3