Fix some errors encountered in coq-dev

jwiegley · Mar 29, 2022 · 4950096 · 4950096
1 parent bdb88a3
commit 4950096
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git a/src/Control/Monad/Indexed.v b/src/Control/Monad/Indexed.v
@@ -1,5 +1,6 @@
 Require Import Hask.Ltac.
 Require Import Hask.Prelude.
+Require Import FunctionalExtensionality.
 
 Generalizable All Variables.
 Set Primitive Projections.
@@ -126,8 +127,6 @@ Ltac rewrite_iapp_homomorphisms :=
 
 Section IApplicatives.
 
-  Require Import FunctionalExtensionality.
-
   Variable F : Type -> Type -> Type -> Type.
   Context `{IApplicative F}.
 

diff --git a/src/Haskell.v b/src/Haskell.v
@@ -63,10 +63,10 @@ Extract Inlined Constant projT1    => "Prelude.fst".
 Extract Inlined Constant snd       => "Prelude.snd".
 (* Extract Inlined Constant subn      => "(Prelude.-)". *)
 
-Extraction Implicit eq_rect [ x y ].
-Extraction Implicit eq_rect_r [ x y ].
-Extraction Implicit eq_rec [ x y ].
-Extraction Implicit eq_rec_r [ x y ].
+(* Extraction Implicit eq_rect [ x y ]. *)
+(* Extraction Implicit eq_rect_r [ x y ]. *)
+(* Extraction Implicit eq_rec [ x y ]. *)
+(* Extraction Implicit eq_rec_r [ x y ]. *)
 
 Extract Inlined Constant eq_rect => "".
 Extract Inlined Constant eq_rect_r => "".