add machinery to create merged Coq script GArrow.v

[coq-hetmet.git] / src / Banner.v

diff --git a/src/Banner.v b/src/Banner.v
new file mode 100644 (file)
index 0000000..675d5b0
--- /dev/null
+++ b/src/Banner.v
@@ -0,0 +1,33 @@
+(***********************************************************************************************************************************
+ *
+ * This is the Coq development accompanying
+ *
+ *   __Multi-Level Programs are Generalized Arrows__
+ *
+ * Best viewed on a 132-character-wide display (use the first line of this file to size your window)
+ *
+ * This file makes extensive use of Unicode (UTF-8); please make sure your text editor supports it.
+ *
+ * Here is the version of Coq I used:
+ * 
+ *   megacz@skolem:~$ coqc -v
+ *   The Coq Proof Assistant, version 8.3pl1 (March 2011)
+ *   compiled on Mar 17 2011 21:07:25 with OCaml 3.11.2
+ *
+ * Warning: this script may take a half-hour or more to typecheck, even on a very fast machine.
+ *          It also needs about 1.5GB of ram; if you have less than that it will run unbearably slowly.
+ *
+ *  I recommend checking it using the following command:
+ *
+ *    coqc -noglob -dont-load-proofs GArrows.v
+ *
+ **********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Setoid.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Omega.