6 files changed, 13 insertions, 56 deletions
diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt
index 002a94cb7..a58303520 100644
--- a/doc/CMakeLists.txt
+++ b/doc/CMakeLists.txt
@@ -17,7 +17,7 @@
 # Set variables required for the documentation *.in files
 
 string(TIMESTAMP MAN_DATE "%Y-%m-%d")
-set(VERSION CVC4_RELEASE_STRING)
+set(VERSION CVC5_RELEASE_STRING)
 
 #-----------------------------------------------------------------------------#
 # Generate files
@@ -27,20 +27,20 @@ configure_file(
   ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc_template)
 
 configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/cvc4.1_template.in
-  ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1_template)
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5.1_template.in
+  ${CMAKE_CURRENT_BINARY_DIR}/cvc5.1_template)
 
 configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/cvc4.5.in
-  ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5)
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5.5.in
+  ${CMAKE_CURRENT_BINARY_DIR}/cvc5.5)
 
 configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4.3.in
-  ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3)
+  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc5.3.in
+  ${CMAKE_CURRENT_BINARY_DIR}/libcvc5.3)
 
 configure_file(
-  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4parser.3.in
-  ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3)
+  ${CMAKE_CURRENT_SOURCE_DIR}/libcvc5parser.3.in
+  ${CMAKE_CURRENT_BINARY_DIR}/libcvc5parser.3)
 
 configure_file(
   ${CMAKE_CURRENT_SOURCE_DIR}/options.3cvc_template.in
@@ -49,11 +49,11 @@ configure_file(
 #-----------------------------------------------------------------------------#
 # Install man pages
 
-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1)
-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5)
+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc5.1 DESTINATION share/man/man1)
+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc5.5 DESTINATION share/man/man5)
 install(FILES
-        ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3
-        ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3
+        ${CMAKE_CURRENT_BINARY_DIR}/libcvc5.3
+        ${CMAKE_CURRENT_BINARY_DIR}/libcvc5parser.3
         ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc
         ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc
         DESTINATION share/man/man3)
diff --git a/doc/cvc4.1_template.in b/doc/cvc5.1_template.in
index 042d6cfc1..042d6cfc1 100644
--- a/doc/cvc4.1_template.in
+++ b/doc/cvc5.1_template.in
diff --git a/doc/cvc4.5.in b/doc/cvc5.5.in
index d66110f63..d66110f63 100644
--- a/doc/cvc4.5.in
+++ b/doc/cvc5.5.in
diff --git a/doc/libcvc4.3.in b/doc/libcvc5.3.in
index 1db5b3c2d..1db5b3c2d 100644
--- a/doc/libcvc4.3.in
+++ b/doc/libcvc5.3.in
diff --git a/doc/libcvc4parser.3.in b/doc/libcvc5parser.3.in
index f288daf83..f288daf83 100644
--- a/doc/libcvc4parser.3.in
+++ b/doc/libcvc5parser.3.in
diff --git a/doc/mainpage.md b/doc/mainpage.md
deleted file mode 100644
index 13005e023..000000000
--- a/doc/mainpage.md
+++ /dev/null
@@ -1,43 +0,0 @@
-/**
-\mainpage Getting started with the CVC4 API
-
-The main classes of the CVC4 API are:
-- CVC4::Expr - an expression (a formula, term, variable, constant, etc.)
-- CVC4::Type - a type (every Expr has a Type)
-- CVC4::ExprManager - a factory class for Exprs and Types (create one of these for your application)
-- CVC4::SmtEngine - the SMT interface, permits making assertions and checking satisfiability (create one of these for your application)
-
-There are numerous examples of the use of the C++ API in the examples/api directory of the CVC4 source distribution.  There is also a discussion on our CVC4 Wiki at
-http://cvc4.cs.stanford.edu/wiki/Tutorials#C.2B.2B_API
-
-Using the CVC4 API from Java
-
-While these API documentation resources explicitly refer to the C++ interface, the Java interface is generated automatically from the C++ sources by SWIG, and thus the interface is almost line-by-line identical in Java.  It is possible, then, to use these C++ resources to help with the Java API.  There are three main ways in which the Java API differs from the C++ API.  First, the CVC4 API makes moderate use of C++ operator overloading, which is not possible in Java.  We have provided standard renamings for the Java methods associated to these C++ overloaded operators---for instance, "plus" replaces operator+, "equals" replaces operator==, etc.
-
-Secondly, C++ iterators are replaced by Java iterators.  Instead of begin() and end() on classes like CVC4::Expr, you'll notice in the Java interface that there is an iterator() method that returns a java.util.Iterator<Expr>.  This allows Java developers to more naturally work with our (ultimately C++) objects through a more Java-like interface.
-
-Third, I/O streams are wrapped so that some functions requiring C++ input and output streams will accept Java InputStreams and OutputStreams.
-
-Our intent is to make the C++ API as useful and functional for Java developers as possible, while still retaining the flexibility of our original C++ design.  If we can make your life as a Java user of our libraries easier, please let us know by requesting an enhancement or reporting a bug at our bug-tracking service, https://github.com/CVC4/CVC4/issues.
-
-For examples of Java programs using the CVC4 API, look in the directory examples/api/java in the CVC4 source distribution.
-
-Thank you for your interest in CVC4!
-
-The CVC4 Development team
-
-\page authors AUTHORS
-\verbinclude AUTHORS
-\page copying COPYING
-\verbinclude COPYING
-\page install INSTALL
-\verbinclude INSTALL
-\page news NEWS
-\verbinclude NEWS
-\page release-notes RELEASE-NOTES
-\verbinclude RELEASE-NOTES
-\page readme README
-\verbinclude README
-\page thanks THANKS
-\verbinclude THANKS
-*/