diff options
| author | Vincent Laporte | 2019-08-05 11:35:10 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-08-05 11:35:10 +0000 |
| commit | fcdfbddbd75218a6d67c965ce363fb2a8984e224 (patch) | |
| tree | d6338f37975a8ffefa31543bddfdd65c6935de96 /plugins | |
| parent | 5f7c88d0835631ed4fdaf6dc056c958bf8865b56 (diff) | |
| parent | 08c9ac8e0919ed7e6c001542c2094640f1d7bd73 (diff) | |
Merge PR #10445: Split constructive and classical axioms for real numbers
Ack-by: Zimmi48
Ack-by: silene
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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"] |