summaryrefslogtreecommitdiff
path: root/src/include/vc.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2009-11-03 03:37:08 +0000
committerMorgan Deters <mdeters@gmail.com>2009-11-03 03:37:08 +0000
commit842e581321bcd9f30c60b9dacc671843ca776fed (patch)
tree202ddf8dae7e090e06d5aed869337ef9162309cd /src/include/vc.h
parent541379b3d361e255cd664207f8b2e278a5b5e3eb (diff)
additional headers and modifications; now passes syntax check
Diffstat (limited to 'src/include/vc.h')
-rw-r--r--src/include/vc.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/include/vc.h b/src/include/vc.h
index a75aa0548..57d8a957e 100644
--- a/src/include/vc.h
+++ b/src/include/vc.h
@@ -10,6 +10,9 @@
#ifndef __CVC4_VC_H
#define __CVC4_VC_H
+#include "command.h"
+#include "expr.h"
+
/* TODO provide way of querying whether you fall into a fragment /
* returning what fragment you're in */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback