From 43ef8b9a4b998b9e60c4f6669777de10f26f7e79 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Dec 2013 05:03:18 -0800
Subject: [PATCH] refactor(library/tactic): rename boolean.* to
 boolean_tactics.*

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/CMakeLists.txt                       | 2 +-
 src/library/tactic/{boolean.cpp => boolean_tactics.cpp} | 2 +-
 src/library/tactic/{boolean.h => boolean_tactics.h}     | 2 +-
 src/library/tactic/register_module.h                    | 4 ++--
 src/tests/library/tactic/tactic.cpp                     | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)
 rename src/library/tactic/{boolean.cpp => boolean_tactics.cpp} (99%)
 rename src/library/tactic/{boolean.h => boolean_tactics.h} (93%)

diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index 07b267a73..5d3a881c9 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp
-proof_state.cpp tactic.cpp boolean.cpp apply_tactic.cpp)
+proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})
diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean_tactics.cpp
similarity index 99%
rename from src/library/tactic/boolean.cpp
rename to src/library/tactic/boolean_tactics.cpp
index 7e6185fe1..1e842184e 100644
--- a/src/library/tactic/boolean.cpp
+++ b/src/library/tactic/boolean_tactics.cpp
@@ -386,7 +386,7 @@ static int mk_absurd_tactic(lua_State * L) {
     return push_tactic(L, absurd_tactic());
 }
 
-void open_boolean(lua_State * L) {
+void open_boolean_tactics(lua_State * L) {
     SET_GLOBAL_FUN(mk_conj_tactic,     "conj_tactic");
     SET_GLOBAL_FUN(mk_imp_tactic,      "imp_tactic");
     SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
diff --git a/src/library/tactic/boolean.h b/src/library/tactic/boolean_tactics.h
similarity index 93%
rename from src/library/tactic/boolean.h
rename to src/library/tactic/boolean_tactics.h
index 141324fbf..1cafb7f63 100644
--- a/src/library/tactic/boolean.h
+++ b/src/library/tactic/boolean_tactics.h
@@ -17,5 +17,5 @@ tactic disj_tactic();
 tactic disj_tactic(unsigned i);
 tactic disj_tactic(name const & gname);
 tactic absurd_tactic();
-void open_boolean(lua_State * L);
+void open_boolean_tactics(lua_State * L);
 }
diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h
index 4d913b930..7cfc7de4d 100644
--- a/src/library/tactic/register_module.h
+++ b/src/library/tactic/register_module.h
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "library/tactic/cex_builder.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
-#include "library/tactic/boolean.h"
+#include "library/tactic/boolean_tactics.h"
 #include "library/tactic/apply_tactic.h"
 
 namespace lean {
@@ -21,7 +21,7 @@ inline void open_tactic_module(lua_State * L) {
     open_cex_builder(L);
     open_proof_state(L);
     open_tactic(L);
-    open_boolean(L);
+    open_boolean_tactics(L);
     open_apply_tactic(L);
 }
 inline void register_tactic_module() {
diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp
index fa9f2bfb5..b2427f215 100644
--- a/src/tests/library/tactic/tactic.cpp
+++ b/src/tests/library/tactic/tactic.cpp
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/tactic.h"
-#include "library/tactic/boolean.h"
+#include "library/tactic/boolean_tactics.h"
 using namespace lean;
 
 tactic loop_tactic() {