configure option adjustments as per 11/24 meeting; various fixes and improvements

5 files changed, 10 insertions, 6 deletions

diff --git a/src/main/about.h b/src/main/about.h
index 458716842..e81e04288 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#ifndef __CVC4__MAIN__ABOUT_H
 #define __CVC4__MAIN__ABOUT_H
 
 namespace CVC4 {
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index f1fe375b6..dcb23c303 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <cstdio>
 #include <cstdlib>
 #include <new>
 #include <unistd.h>
@@ -29,7 +30,7 @@ using namespace std;
 using namespace CVC4;
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 static const char lang_help[] = "\
 Languages currently supported to the -L / --lang option:\n\
@@ -135,5 +136,5 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
   return optind;
 }
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 44543a75f..8529f2ca2 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#include <cstdio>
 #include <cstdlib>
 #include <cerrno>
 #include <new>
@@ -25,7 +26,7 @@
 
 using namespace std;
 using namespace CVC4;
-using namespace CVC4::Main;
+using namespace CVC4::main;
 
 int main(int argc, char *argv[]) {
   struct Options opts;
@@ -57,7 +58,7 @@ int main(int argc, char *argv[]) {
       //   delete cmd;
       // }
     }
-  } catch(CVC4::Main::OptionException* e) {
+  } catch(CVC4::main::OptionException* e) {
     if(opts.smtcomp_mode) {
       printf("unknown");
       fflush(stdout);
diff --git a/src/main/usage.h b/src/main/usage.h
index 3326108ac..0b503cdb2 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -10,6 +10,7 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#ifndef __CVC4__MAIN__USAGE_H
 #define __CVC4__MAIN__USAGE_H
 
 namespace CVC4 {
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 572aea00f..e2333b417 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -23,7 +23,7 @@ using CVC4::Exception;
 using namespace std;
 
 namespace CVC4 {
-namespace Main {
+namespace main {
 
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
@@ -51,5 +51,5 @@ void cvc4_init() throw() {
     throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
 }
 
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
 }/* CVC4 namespace */