diff options
| author | Vincent Semeria | 2019-06-27 23:35:03 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-07-16 18:45:34 +0200 |
| commit | eebc676ce4978b7e408c427889bae356d8b0efdc (patch) | |
| tree | 2bc6228c80817026d4e2108e871867fc50a86fa2 /plugins | |
| parent | 3bd2722fb53552f45a25e6bc0a03a9ab0517485f (diff) | |
Define constructive real numbers as Cauchy sequences of rational numbers. Redefine classical real numbers as a quotient of those constructive real numbers.
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"] |