From c690a68ba0b78b913cbcb60f7508d431071d4c79 Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Fri, 4 Oct 2019 18:29:58 +0200
Subject: Replace classical reals quotient axioms by functional extensionality.
 Define homotopy propositions and homotopy sets. Rename local variable R in
 test Nsatz, to avoid a name collision with the type of real numbers.

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

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 66db924051..70c1077106 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -102,7 +102,7 @@ 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 r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R"
 
 let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
 let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult")
-- 
cgit v1.2.3