diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-21 15:16:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-21 15:16:20 -0500 |
| commit | d7f3cf539939c717692d1309bda742801817ad64 (patch) | |
| tree | 0a0be770c146f0dfe72bd2d7ac10da4d5b5ff80c /src/theory | |
| parent | 0b7e50aa1f0f2e6a77fb7e2a1f48b6af8ce5b91d (diff) | |
(proof-new) Minor documentation sync (#6592)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/eager_proof_generator.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 1606fbb50..c0b368e6e 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -130,7 +130,7 @@ class EagerProofGenerator : public ProofGenerator * @param isConflict Whether the returned trust node is a conflict (otherwise * it is a lemma), * @return The trust node corresponding to the fact that this generator has - * a proof of (children => exp), or of exp if children is empty. + * a proof of (exp => conc), or of conc if exp is empty. */ TrustNode mkTrustNode(Node conc, PfRule id, |