From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 10 Mar 2021 21:33:41 +0000 (-0300)
Subject: [proof-new] Clarifying doc (#6108)
X-Git-Tag: cvc5-1.0.0~2112
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4519b17b6738cf959877c0e0b37000fc7bb0d88;p=cvc5.git

[proof-new] Clarifying doc (#6108)
---

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 2759a3c9e..e2933e012 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -302,8 +302,8 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: C2
   // where
-  //  Set representations of C1 and C2 is the same but the number of literals in
-  //  C2 is the same of that of C1
+  //  Set representations of C1 and C2 are the same and the number of literals
+  //  in C2 is the same of that of C1
   REORDERING,
   // ======== N-ary Resolution + Factoring + Reordering
   // Children: (P1:C_1, ..., Pm:C_n)