summaryrefslogtreecommitdiff
path: root/src/parser/cvc
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc')
-rw-r--r--src/parser/cvc/Cvc.g2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index e3d0e0696..64eb56c74 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -757,7 +757,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
END_TOK
{ PARSER_STATE->popScope();
cmd->reset(new DatatypeDeclarationCommand(
- PARSER_STATE->mkMutualDatatypeTypes(dts)));
+ api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts))));
}
| CONTEXT_TOK
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback