From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 14 Dec 2010 19:37:35 +0000 (+0000)
Subject: permit PARAMETERIZED operators to be zero-ary
X-Git-Tag: cvc5-1.0.0~8721
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b44f183a75deea11fa379554b893b6656e1864b2;p=cvc5.git

permit PARAMETERIZED operators to be zero-ary
---

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index c68ba59cd..4ce0c6262 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -235,17 +235,9 @@ function register_metakind {
     exit 1
   fi
 
-  if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
-    if [ $mk = PARAMETERIZED -a "$k" = SORT_TYPE ]; then
-      # exception: zero-ary SORT_TYPE is permitted for sort constructors
-      :
-    elif [ $mk = PARAMETERIZED -a "$k" = APPLY ]; then
-      # exception: zero-ary APPLY is permitted for defined zero-ary functions
-      :
-    elif [ $lb = 0 ]; then
-      echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
-      exit 1
-    fi
+  if [ $mk = OPERATOR -a $lb = 0 ]; then
+    echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
+    exit 1
   fi
 
   metakind_lbchildren="${metakind_lbchildren}