summaryrefslogtreecommitdiffstats
path: root/external
diff options
context:
space:
mode:
authorYong He <yonghe@outlook.com>2020-09-04 10:18:44 -0700
committerGitHub <noreply@github.com>2020-09-04 10:18:44 -0700
commit8f962894fd38edb47d782d303ac9ff87b3a3bb6a (patch)
tree449d0d58ca7d90a11759372c9dc82650a565f96a /external
parent5e10f1b4f0654515af1fcb29e8d1f35e691c8aa3 (diff)
Allow mixing unspecialized and specialized existential parameters. (#1533)
* Allow mixing unspecialized and specialized existential parameters. * Fixes.
Diffstat (limited to 'external')
0 files changed, 0 insertions, 0 deletions