Minor

ajreynol · Dec 18, 2024 · ba13582 · ba13582
1 parent 206046d
commit ba13582
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -1394,7 +1394,7 @@ enum ENUM(ProofRule)
    * .. math::
    *   \inferrule{-\mid s} {C \rightarrow R[k]}
    * 
-   * where :math:`s` is the internal representation of an existential
+   * where :math:`s` is the internal specification of an existential
    * :math:`\exists x.\> R[x]`.
    *
    * \endverbatim

diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp
@@ -130,6 +130,7 @@ const char* toString(ProofRule rule)
     case ProofRule::QUANT_VAR_REORDERING: return "QUANT_VAR_REORDERING";
     case ProofRule::EXISTS_STRING_LENGTH: return "EXISTS_STRING_LENGTH";
     case ProofRule::EXISTS_INV_CONDITION: return "EXISTS_INV_CONDITION";
+    case ProofRule::MACRO_EXISTS_INV_CONDITION: return "MACRO_EXISTS_INV_CONDITION";
     //================================================= Sets rules
     case ProofRule::SETS_SINGLETON_INJ: return "SETS_SINGLETON_INJ";
     case ProofRule::SETS_EXT: return "SETS_EXT";