diff options
Diffstat (limited to 'src/theory/uf/proof_equality_engine.h')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.h | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index b71f72c53..314353131 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -307,12 +307,6 @@ class ProofEqEngine : public EagerProofGenerator const std::vector<TNode>& assumps, TrustNodeKind tnk, LazyCDProof* curr); - /** - * Make the conjunction of nodes in a. Returns true if a is empty, and a - * single literal if a has size 1. - */ - Node mkAnd(const std::vector<Node>& a); - Node mkAnd(const std::vector<TNode>& a); /** Reference to the equality engine */ eq::EqualityEngine& d_ee; /** The default proof generator (for simple facts) */ |