From b777375469f99316a2a27aa4a4c7ab232803871d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Oct 2015 16:24:51 -0700
Subject: [PATCH] fix(frontends/lean/parser): decimals

---
 src/frontends/lean/parser.cpp | 2 +-
 src/library/constants.cpp     | 4 ++++
 src/library/constants.h       | 1 +
 src/library/constants.txt     | 1 +
 4 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 482d431479..3bd05df6f0 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1574,7 +1574,7 @@ expr parser::parse_decimal_expr() {
         return num;
     } else {
         expr den = save_pos(mk_prenum(val.get_denominator()), p);
-        expr div = save_pos(mk_constant(get_div_name()), p);
+        expr div = save_pos(mk_constant(get_division_name()), p);
         return save_pos(lean::mk_app(div, num, den), p);
     }
 }
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 572efa2734..edc158e034 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -18,6 +18,7 @@ name const * g_char_mk = nullptr;
 name const * g_congr = nullptr;
 name const * g_dite = nullptr;
 name const * g_div = nullptr;
+name const * g_division = nullptr;
 name const * g_empty = nullptr;
 name const * g_empty_rec = nullptr;
 name const * g_eq = nullptr;
@@ -172,6 +173,7 @@ void initialize_constants() {
     g_congr = new name{"congr"};
     g_dite = new name{"dite"};
     g_div = new name{"div"};
+    g_division = new name{"division"};
     g_empty = new name{"empty"};
     g_empty_rec = new name{"empty", "rec"};
     g_eq = new name{"eq"};
@@ -327,6 +329,7 @@ void finalize_constants() {
     delete g_congr;
     delete g_dite;
     delete g_div;
+    delete g_division;
     delete g_empty;
     delete g_empty_rec;
     delete g_eq;
@@ -481,6 +484,7 @@ name const & get_char_mk_name() { return *g_char_mk; }
 name const & get_congr_name() { return *g_congr; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_div_name() { return *g_div; }
+name const & get_division_name() { return *g_division; }
 name const & get_empty_name() { return *g_empty; }
 name const & get_empty_rec_name() { return *g_empty_rec; }
 name const & get_eq_name() { return *g_eq; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 85a89eeec9..60d0a80fe9 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -20,6 +20,7 @@ name const & get_char_mk_name();
 name const & get_congr_name();
 name const & get_dite_name();
 name const & get_div_name();
+name const & get_division_name();
 name const & get_empty_name();
 name const & get_empty_rec_name();
 name const & get_eq_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 153873db9e..c045298bc8 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -13,6 +13,7 @@ char.mk
 congr
 dite
 div
+division
 empty
 empty.rec
 eq