summaryrefslogtreecommitdiff
path: root/tests/ffisub.urs
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2015-10-24 11:06:31 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2015-10-24 11:06:31 -0400
commit7d861ea0debf944cb8e3e38d73a8c0197de574b3 (patch)
treeed87d21ffe040bf296d2230c7490abda8e34752c /tests/ffisub.urs
parent598756dc69f89cf2dd2b889cad63a7a690ae7ed7 (diff)
parentcb0109804fdad0dd423bb344446344cdc08c0886 (diff)
Merge branch 'upstream' into dfsg_clean20151018+dfsg
Diffstat (limited to 'tests/ffisub.urs')
-rw-r--r--tests/ffisub.urs5
1 files changed, 5 insertions, 0 deletions
diff --git a/tests/ffisub.urs b/tests/ffisub.urs
new file mode 100644
index 00000000..ce245884
--- /dev/null
+++ b/tests/ffisub.urs
@@ -0,0 +1,5 @@
+structure S : sig
+ type t
+end
+
+val x : S.t