Updated headers

diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp
index 678595f5fd953cf0e9d2d0a8c1bff8101fb0646d..7a8970c2976b3406c8b4c87ae2c49dbdefbf9b89 100644 (file)
--- a/src/theory/shared_data.cpp
+++ b/src/theory/shared_data.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file shared_data.cpp
  ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
+ ** Original author: barrett
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
@@ -11,9 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Implementation of equivalence class data for UF theory.
+ ** \brief Implementation of shared data for shared term manager.
  **
- ** Implementation of equivalence class data for UF theory.  This is a
+ ** Implementation of shared data used by the shared term manager.  This is a
  ** context-dependent object.
  **/
 

diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h
index d8ed6338773cfe17bd1e93e7274bfc133c7289da..64b7f5ab16f9de719c18f21273c8a98d5cc7a4f2 100644 (file)
--- a/src/theory/shared_data.h
+++ b/src/theory/shared_data.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file shared_data.h
  ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
+ ** Original author: barrett
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
@@ -11,10 +11,10 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Context dependent equivalence class datastructure for nodes.
+ ** \brief Context-dependent data class for shared terms
  **
- ** Context dependent equivalence class datastructure for nodes.
- ** Currently keeps a context dependent watch list.
+ ** Context-dependent data class for shared terms.
+ ** Used by SharedTermManager.
  **/
 
 #include "cvc4_private.h"