X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtraction.v;h=82b05434263ca1fb6e754f08f89ea3a1a8e7b616;hb=bb960df7c29c851ca9d13f2d0c8f351ac24045ca;hp=d1c84e450a7693b5859442dabbee3ecd2667bb21;hpb=539d675a181f178e24c15b2a6ad3c990492eed79;p=coq-hetmet.git

diff --git a/src/Extraction.v b/src/Extraction.v
index d1c84e4..82b0543 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -1,3 +1,10 @@
+(*********************************************************************************************************************************)
+(* Extraction:                                                                                                                   *)
+(*                                                                                                                               *)
+(*    This module is the "top level" for extraction                                                                              *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
 (* need this or the Haskell extraction fails *)
 Set Printing Width 1300000.
 
@@ -25,10 +32,14 @@ Require Import HaskProof.
 Require Import HaskCoreToWeak.
 Require Import HaskWeakToStrong.
 Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
 Require Import HaskProofToLatex.
 Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
+Require Import HaskProofToStrong.
+
+Require Import HaskProofCategory.
+Require Import HaskStrongCategory.
+Require Import ReificationsEquivalentToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.