diff options
Diffstat (limited to 'src/include/cvc5parser_private.h')
| -rw-r--r-- | src/include/cvc5parser_private.h | 11 |
1 files changed, 5 insertions, 6 deletions
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 */ |