summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r--src/expr/expr_manager_template.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 71f41354a..2e6832840 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -520,7 +520,7 @@ public:
/**
* Create a new, fresh variable for use in a binder expression
- * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). It is
+ * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE). It is
* an error for this bound variable to exist outside of a binder,
* and it should also only be used in a single binder expression.
* That is, two distinct FORALL expressions should use entirely
@@ -539,7 +539,7 @@ public:
/**
* Create a (nameless) new, fresh variable for use in a binder
- * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
+ * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE).
* It is an error for this bound variable to exist outside of a
* binder, and it should also only be used in a single binder
* expression. That is, two distinct FORALL expressions should use
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback