From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 3 Aug 2020 23:26:42 +0000 (-0700)
Subject: Update documentation for Solver::mkVar() (#4833)
X-Git-Tag: cvc5-1.0.0~3047
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c84db77ecdaa7107a33824484bf9c649f8fcbbff;p=cvc5.git

Update documentation for Solver::mkVar() (#4833)

The documentation of `Solver::mkVar()` was not very clear regarding what
it could be used for. This lead to some confusion (see e.g. #4828).
This commit makes the documentation more explicit.
---

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index edd74280a..bba654200 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2788,7 +2788,8 @@ class CVC4_PUBLIC Solver
   Term mkConst(Sort sort, const std::string& symbol = std::string()) const;
 
   /**
-   * Create (bound) variable.
+   * Create a bound variable to be used in a binder (i.e. a quantifier, a
+   * lambda, or a witness binder).
    * @param sort the sort of the variable
    * @param symbol the name of the variable
    * @return the variable