Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / exportprove / prove / provastruct3.v

diff --git a/helm/EXPORT/exportprove/prove/provastruct3.v b/helm/EXPORT/exportprove/prove/provastruct3.v
new file mode 100644 (file)
index 0000000..d189330
--- /dev/null
+++ b/helm/EXPORT/exportprove/prove/provastruct3.v
@@ -0,0 +1,11 @@
+Section a.
+ Section a1.
+  Variable A : Prop.
+  Variable B : Prop.
+  Inductive t1 : Set := k1 : A -> t1.
+ End a1.
+ 
+ Inductive t2 [B:Set] : Set := k2 : (t2 B).
+
+ Variable A : Prop.
+End a.