diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 4 |
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 |