update to use Control.GArrow instead of GHC.HetMet.GArrow

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

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 9f0fc1a..42a29ed 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -547,9 +547,9 @@ Section core2proof.
       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
       dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
       dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>

-      dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
-      dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
-      dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
+      dsLookupTyc "Control.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
+      dsLookupTyc "Control.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
+      dsLookupTyc "Control.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>

       dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
       dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
       dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
       dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
       dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
       dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>