diff options
Diffstat (limited to 'src/expr/node_manager.h')
| -rw-r--r-- | src/expr/node_manager.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index adba8087c..3646e91c5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -580,7 +580,7 @@ public: inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); /** Make a type representing a constructor with the given parameterization */ - TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range); + TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range); /** Make a type representing a selector with the given parameterization */ inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); |