+/****v* Globals/document_header
+ * NAME
+ * document_header -- Header for the documentation.
+ * PURPOSE
+ * Used as the header of generated files
+ * SOURCE
+ */
+
+char *document_header = NULL;
+
+/******/
+
+
+/****v* Globals/document_footer
+ * NAME
+ * document_footer -- Footer for the documentation.
+ * PURPOSE
+ * Used as the footer of generated files
+ * SOURCE
+ */
+
+char *document_footer = NULL;
+
+/******/
+
+