diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-09 11:18:18 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-09 17:46:21 -0400 |
| commit | ec4d1e3753434f5d34a22e653dace14b87557aaf (patch) | |
| tree | 9cfa4fc484dd5e27373277751887e50558a458df /src/expr/mkmetakind | |
| parent | e93d0be650b9f349fe8be3a56ce2fc7cb20fddf0 (diff) | |
Minor change to better support parameterized partial/total kinds (for upcoming datatypes work).
Diffstat (limited to 'src/expr/mkmetakind')
| -rwxr-xr-x | src/expr/mkmetakind | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 4dc2908a7..5f003dcfb 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -203,7 +203,9 @@ function parameterized { check_theory_seen register_metakind PARAMETERIZED "$1" "$3" - registerOperatorToKind "$1" "$2" + if ! expr "$2" : '\[.*\]' &>/dev/null; then + registerOperatorToKind "$1" "$2" + fi } function constant { |