summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ematching/ho_trigger.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.h')
-rw-r--r--src/theory/quantifiers/ematching/ho_trigger.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 64f03e7fa..78b2e6c84 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -145,7 +145,7 @@ class HigherOrderTrigger : public Trigger
std::map<TNode, std::vector<Node> > d_ho_var_bvs;
std::map<TNode, Node> d_ho_var_bvl;
/** the set of types of ho variables */
- std::unordered_set<TypeNode, TypeNodeHashFunction> d_ho_var_types;
+ std::unordered_set<TypeNode> d_ho_var_types;
/** add higher-order type predicate lemmas
*
* Adds lemmas of the form P( f ), where P is the predicate
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback