From 7a5f75524c59bf885d7c31ed1ae8a7cfe725d5dc Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 21 Jun 2019 10:57:15 +0100
Subject: Coq: be more careful when dealing with wildcard argument patterns If
 they're merged with a type variable then we still need to name the argument
 so that it can be used in other types.

---
 test/coq/pass/wildcardmerge.sail | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test/coq/pass/wildcardmerge.sail

(limited to 'test')

diff --git a/test/coq/pass/wildcardmerge.sail b/test/coq/pass/wildcardmerge.sail
new file mode 100644
index 00000000..ca83b47d
--- /dev/null
+++ b/test/coq/pass/wildcardmerge.sail
@@ -0,0 +1,10 @@
+default Order dec
+$include <prelude.sail>
+
+/* Checks that when merging the type variable with the integer argument,
+   that we name the integer so that we can write the type of the
+   second argument. */
+
+val f : forall 'n, 'n >= 0. (int('n), bits('n)) -> unit
+
+function f(_,_) = ()
-- 
cgit v1.2.3