4 files changed, 12 insertions, 15 deletions
diff --git a/src/include/cvc5_private.h b/src/include/cvc5_private.h
index 1c328ef60..6377997ef 100644
--- a/src/include/cvc5_private.h
+++ b/src/include/cvc5_private.h
@@ -18,8 +18,8 @@
 #define CVC5_PRIVATE_H
 
 #if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
-#  error A private CVC4 header was included when not building the library or private unit test code.
-#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
+#  error A private cvc5 header was included when not building the library or private unit test code.
+#endif
 
 #include "cvc4autoconfig.h"
 #include "cvc5_public.h"
diff --git a/src/include/cvc5_private_library.h b/src/include/cvc5_private_library.h
index 95c928fb5..36b2bbd04 100644
--- a/src/include/cvc5_private_library.h
+++ b/src/include/cvc5_private_library.h
@@ -21,10 +21,8 @@
       || defined(__BUILDING_CVC4PARSERLIB)                                 \
       || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)                       \
       || defined(__BUILDING_CVC4DRIVER))
-#  error A "private library" CVC4 header was included when not building the library, driver, or private unit test code.
-#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST ||          \
-          __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || \
-          __BUILDING_CVC4DRIVER) */
+#  error A "private library" cvc5 header was included when not building the library, driver, or private unit test code.
+#endif
 
 #include "cvc4autoconfig.h"
 #include "cvc5_public.h"
diff --git a/src/include/cvc5parser_private.h b/src/include/cvc5parser_private.h
index aec3a09a5..8f6142cbb 100644
--- a/src/include/cvc5parser_private.h
+++ b/src/include/cvc5parser_private.h
@@ -14,14 +14,13 @@
  * when the file is included improperly.
  */
 
-#ifndef __CVC4PARSER_PRIVATE_H
-#define __CVC4PARSER_PRIVATE_H
+#ifndef CVC5PARSER_PRIVATE_H
+#define CVC5PARSER_PRIVATE_H
 
 #if !(defined(__BUILDING_CVC4PARSERLIB) \
       || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST))
-#  error A private CVC4 parser header was included when not building the parser library or private unit test code.
-#endif /* ! (__BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST) \
-        */
+#  error A private cvc5 parser header was included when not building the parser library or private unit test code.
+#endif
 
 #include "cvc5parser_public.h"
 // It would be nice to #include "cvc4autoconfig.h" here, but there are conflicts
@@ -29,4 +28,4 @@
 //
 // #include "cvc4autoconfig.h"
 
-#endif /* __CVC4PARSER_PRIVATE_H */
+#endif /* CVC5PARSER_PRIVATE_H */
diff --git a/src/include/cvc5parser_public.h b/src/include/cvc5parser_public.h
index 099eb58c2..71bd4981a 100644
--- a/src/include/cvc5parser_public.h
+++ b/src/include/cvc5parser_public.h
@@ -14,9 +14,9 @@
  * libraries and driver binary, and also exported to the user.
  */
 
-#ifndef __CVC4PARSER_PUBLIC_H
-#define __CVC4PARSER_PUBLIC_H
+#ifndef CVC5PARSER_PUBLIC_H
+#define CVC5PARSER_PUBLIC_H
 
 #include "cvc5_public.h"
 
-#endif /* __CVC4PARSER_PUBLIC_H */
+#endif /* CVC5PARSER_PUBLIC_H */