aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/coq/multiple/b2.v
diff options
context:
space:
mode:
Diffstat (limited to 'etc/coq/multiple/b2.v')
-rw-r--r--etc/coq/multiple/b2.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/etc/coq/multiple/b2.v b/etc/coq/multiple/b2.v
index b29c5e68..0bccf579 100644
--- a/etc/coq/multiple/b2.v
+++ b/etc/coq/multiple/b2.v
@@ -1 +1,3 @@
+(* b2 -> b1 -> b -> c *)
+
Parameter b2:Set.