summaryrefslogtreecommitdiff
path: root/src/proof/lrat/lrat_proof.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/lrat/lrat_proof.h')
-rw-r--r--src/proof/lrat/lrat_proof.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index a999e5ca6..7cd773409 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -130,10 +130,6 @@ class LratProof
* @brief Construct an LRAT proof from a DRAT proof, using drat-trim
*
* @param usedClauses The CNF formula that we're deriving bottom from.
- * It's a map because other parts of the system represent
- * it this way.
- * @param clauseOrder A record of the order in which those clauses were
- * given to the SAT solver.
* @param dratBinary The DRAT proof from the SAT solver, as a binary stream.
*/
static LratProof fromDratProof(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback