merge from symmetry branch

1 files changed, 5 insertions, 0 deletions

diff --git a/src/printer/printer.h b/src/printer/printer.h
index adbabe3c5..eae2fc48f 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -23,6 +23,7 @@
 
 #include "util/language.h"
 #include "expr/node.h"
+#include "expr/command.h"
 
 namespace CVC4 {
 
@@ -45,6 +46,10 @@ public:
   /** Write a Node out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, TNode n,
                         int toDepth, bool types) const = 0;
+
+  /** Write a Command out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const Command* c,
+                        int toDepth, bool types) const = 0;
 };/* class Printer */
 
 }/* CVC4 namespace */