summaryrefslogtreecommitdiff
path: root/src/proof/theory_proof.h
diff options
context:
space:
mode:
authorAndres Notzli <andres.noetzli@gmail.com>2016-08-04 15:12:54 -0700
committerAndres Notzli <andres.noetzli@gmail.com>2016-08-05 10:31:30 -0700
commit0812bb7f36c454d282be5e9960a9a820e4fbd52c (patch)
treebf5e3b13026bc007aa57046200974e8bdf17f3db /src/proof/theory_proof.h
parentc82514b57252444df982b35af4809e0fd4635e37 (diff)
Minor: add/fix comments, remove redundant includes
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r--src/proof/theory_proof.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 80a737580..34248f7eb 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -205,7 +205,7 @@ public:
{}
virtual ~TheoryProof() {};
/**
- * Print a term belonging some theory, not neccessarily this one.
+ * Print a term belonging some theory, not necessarily this one.
*
* @param term expresion representing term
* @param os output stream
@@ -216,7 +216,7 @@ public:
/**
* Print a term belonging to THIS theory.
*
- * @param term expresion representing term
+ * @param term expression representing term
* @param os output stream
*/
virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback