This commit was manufactured by cvs2svn to create branch

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

diff --git a/helm/EXPORT/exportprove/prove/provastruct2.v b/helm/EXPORT/exportprove/prove/provastruct2.v
deleted file mode 100644 (file)
index 0784e97..0000000
--- a/helm/EXPORT/exportprove/prove/provastruct2.v
+++ /dev/null
@@ -1,42 +0,0 @@
-Section init.
-Section a.
- Section a1.
-  Section a11.
-   Section a111.
-    Local uno := (S O).
-   End a111.
-   Section a112.
-   End a112.
-   Section a113.
-   End a113.
-  End a11.
-  Local uno := (S O).
- End a1.
- Section a2.
-  Section a21.
-   Local uno := (S O).
-  End a21.
-  Section a22.
-   Section a221.
-   End a221.
-  End a22.
-  Section a23.
-   Section a231.
-    Section a2311.
-     Local uno := (S O).
-    End a2311.
-    Section a2312.
-    End a2312.
-    Section a2313.
-    End a2313.
-   End a231.
-   Section a232.
-    Section a2321.
-    End a2321.
-   End a232.
-  End a23.
-  Local uno := (S O).
- End a2.
- Definition uno := (S O).
-End a.
-End init.