summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/rewrite_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.h')
-rw-r--r--[-rwxr-xr-x]src/theory/quantifiers/rewrite_engine.h21
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 2d9d751c2..a9a2f9b46 100755..100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -1,13 +1,16 @@
/********************* */
-/*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013 New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
+/*! \file rewrite_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
**/
#include "cvc4_private.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback