From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 7 Jul 2010 02:26:38 +0000 (+0000)
Subject: Updated headers
X-Git-Tag: cvc5-1.0.0~8924
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98b384fa54feb03b17ce24930f8ba2dc252374c8;p=cvc5.git

Updated headers
---

diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp
index 678595f5f..7a8970c29 100644
--- 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 d8ed63387..64b7f5ab1 100644
--- 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"