summaryrefslogtreecommitdiff
path: root/src/expr/mkmetakind
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/mkmetakind')
-rwxr-xr-xsrc/expr/mkmetakind6
1 files changed, 0 insertions, 6 deletions
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 4582bfeda..47ffc77f9 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -80,12 +80,6 @@ function theory {
// #include \"theory/$b/$2\""
}
-function instantiator {
- # instantiator class header
- lineno=${BASH_LINENO[0]}
- check_theory_seen
-}
-
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback