From f0fac1ae0e48f51a90d0ae9bb2c80ef399a4af47 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Feb 2015 15:27:18 -0800
Subject: [PATCH] feat(library/constants): add eq.intro

---
 src/library/constants.cpp | 4 ++++
 src/library/constants.h   | 1 +
 src/library/constants.txt | 1 +
 3 files changed, 6 insertions(+)

diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 7b544c7e5..a69333647 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -15,6 +15,7 @@ name const * g_char = nullptr;
 name const * g_char_mk = nullptr;
 name const * g_dite = nullptr;
 name const * g_eq = nullptr;
+name const * g_eq_intro = nullptr;
 name const * g_eq_rec = nullptr;
 name const * g_eq_rec_eq = nullptr;
 name const * g_eq_refl = nullptr;
@@ -122,6 +123,7 @@ void initialize_constants() {
     g_char_mk = new name{"char", "mk"};
     g_dite = new name{"dite"};
     g_eq = new name{"eq"};
+    g_eq_intro = new name{"eq", "intro"};
     g_eq_rec = new name{"eq", "rec"};
     g_eq_rec_eq = new name{"eq_rec_eq"};
     g_eq_refl = new name{"eq", "refl"};
@@ -230,6 +232,7 @@ void finalize_constants() {
     delete g_char_mk;
     delete g_dite;
     delete g_eq;
+    delete g_eq_intro;
     delete g_eq_rec;
     delete g_eq_rec_eq;
     delete g_eq_refl;
@@ -337,6 +340,7 @@ name const & get_char_name() { return *g_char; }
 name const & get_char_mk_name() { return *g_char_mk; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_eq_name() { return *g_eq; }
+name const & get_eq_intro_name() { return *g_eq_intro; }
 name const & get_eq_rec_name() { return *g_eq_rec; }
 name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
diff --git a/src/library/constants.h b/src/library/constants.h
index c086a469c..f65bb4c5e 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -17,6 +17,7 @@ name const & get_char_name();
 name const & get_char_mk_name();
 name const & get_dite_name();
 name const & get_eq_name();
+name const & get_eq_intro_name();
 name const & get_eq_rec_name();
 name const & get_eq_rec_eq_name();
 name const & get_eq_refl_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index e681e3418..19aa1f5ab 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -10,6 +10,7 @@ char
 char.mk
 dite
 eq
+eq.intro
 eq.rec
 eq_rec_eq
 eq.refl