summaryrefslogtreecommitdiff
path: root/src/proof/array_proof.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/array_proof.h')
-rw-r--r--src/proof/array_proof.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 507b65fef..9a2eef9e7 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -19,6 +19,8 @@
#ifndef __CVC4__ARRAY__PROOF_H
#define __CVC4__ARRAY__PROOF_H
+#include <unordered_set>
+
#include "expr/expr.h"
#include "proof/proof_manager.h"
#include "proof/theory_proof.h"
@@ -94,7 +96,7 @@ class TheoryArrays;
} /* namespace CVC4::theory::arrays */
} /* namespace CVC4::theory */
-typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet;
+typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
class ArrayProof : public TheoryProof {
// TODO: whatever goes in this theory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback