add HaskXXXXCategory, generalized arrows, and reifications

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

diff --git a/src/Extraction.v b/src/Extraction.v
index c23d1c5..82b0543 100644 (file)
--- 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.
 
@@ -30,6 +37,10 @@ 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.