summaryrefslogtreecommitdiff
path: root/src/parser/tptp/tptp.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
-rw-r--r--src/parser/tptp/tptp.cpp8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 1177c8010..e6b4969c3 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -28,7 +28,7 @@
#undef true
#undef false
-namespace CVC4 {
+namespace CVC5 {
namespace parser {
Tptp::Tptp(api::Solver* solver,
@@ -202,7 +202,7 @@ void Tptp::checkLetBinding(const std::vector<api::Term>& bvlist,
{
parseError("malformed let: LHS must be formula");
}
- for (const CVC4::api::Term& var : vars)
+ for (const CVC5::api::Term& var : vars)
{
if (var.hasOp())
{
@@ -568,5 +568,5 @@ Command* Tptp::makeAssertCommand(FormulaRole fr,
}
}
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} // namespace parser
+} // namespace CVC5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback