summaryrefslogtreecommitdiff
path: root/src/theory/mkinstantiator
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/mkinstantiator')
-rwxr-xr-xsrc/theory/mkinstantiator6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator
index 73b88986b..73fc6706d 100755
--- a/src/theory/mkinstantiator
+++ b/src/theory/mkinstantiator
@@ -143,6 +143,12 @@ function typerule {
check_theory_seen
}
+function construle {
+ # construle OPERATOR isconst-checking-class
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function rewriter {
# rewriter class header
lineno=${BASH_LINENO[0]}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback