aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/coq/multiple/d.v
diff options
context:
space:
mode:
Diffstat (limited to 'etc/coq/multiple/d.v')
-rw-r--r--etc/coq/multiple/d.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/etc/coq/multiple/d.v b/etc/coq/multiple/d.v
new file mode 100644
index 00000000..4789c998
--- /dev/null
+++ b/etc/coq/multiple/d.v
@@ -0,0 +1,5 @@
+Require a.
+
+Parameter d:Set.
+
+