Refactor documentation (#8288)

[cvc5.git] / docs / index.rst

diff --git a/docs/index.rst b/docs/index.rst
index af8eb498fbaef3fbd6ceddb05544a78be0b31314..746b18daccf2e39ae5beb1b35d9539ffdf06eac9 100644 (file)
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -1,19 +1,28 @@
-.. cvc5 documentation master file, created by
-   sphinx-quickstart on Mon Apr  5 17:02:33 2021.
-   You can adapt this file completely to your liking, but it should at least
-   contain the root `toctree` directive.
+cvc5 Documentation
+==================
 
-cvc5 API Documentation
-======================
+**cvc5** is an open-source automatic theorem prover for Satisfiability Modulo
+Theories (SMT) problems in a large number of theories and their combination.
+**cvc5** is the successor of `CVC4 <https://cvc4.cs.stanford.edu>`_ and is
+intended to be an open and extensible SMT engine.
 
+This space provides all documentation related to using cvc5.
 
-* :ref:`genindex`
-
-
----------------
 
+Table of Contents
+^^^^^^^^^^^^^^^^^
 .. toctree::
-   :maxdepth: 2
+   :maxdepth: 1
 
-   cpp
+   installation/installation
+   binary/binary
+   api/api
+   options
+   output-tags
+   proofs/proofs
+   resource-limits
+   statistics
+   examples/examples
+   theories/theories
    references
+   genindex