Prepare the final ICFP'19 artefact.

Makefile

@@ -1,15 +1,16 @@
-COQFLAGS = ""
+all: Makefile.coq
+	+$(MAKE) -f Makefile.coq all
 
-VFILES = $(wildcard src/*.v)
-VOFILES = $(patsubst %.v,%.vo,$(VFILES))
+clean: Makefile.coq
+	+$(MAKE) -f Makefile.coq cleanall
+	rm -f Makefile.coq Makefile.coq.conf
 
-all: $(VOFILES)
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-%.vo: %.v Makefile.coq
-	$(MAKE) -f Makefile.coq OPT=$(COQFLAGS)
+_CoqProject Makefile: ;
 
-Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o $@
+%: Makefile.coq
+	+$(MAKE) -f Makefile.coq $@
 
-clean: Makefile.coq
-	$(MAKE) -f Makefile.coq clean
+.PHONY: all clean

_CoqProject

@@ -2,13 +2,11 @@
 src/Prelude.v
 src/Ltac.v
 src/Data/Functor.v
-src/Data/Functor/Contravariant.v
-src/Data/Functor/Const.v
 src/Control/Applicative.v
 src/Data/Either.v
 src/Data/Monoid.v
 src/Control/Selective.v
 src/Data/Over.v
 src/Data/Under.v
 src/Data/Validation.v
-src/Control/Selective/FreerRigid.v
+src/Control/Selective/Rigid.v

src/Control/Applicative.v

@@ -1,6 +1,5 @@
 Require Export Hask.Ltac.
 Require Export Hask.Data.Functor.
-Require Export Hask.Data.Functor.Const.
 Require Import FunctionalExtensionality.
 
 Generalizable All Variables.

src/Control/Selective.v

@@ -4,7 +4,6 @@ Require Import Hask.Prelude.
 Require Import Data.Either.
 Require Import Data.Monoid.
 Require Import Hask.Data.Functor.
-Require Import Hask.Data.Functor.Const.
 Require Import Hask.Control.Applicative.
 
 Generalizable All Variables.
@@ -31,11 +30,11 @@ Definition apS `{Selective f} {A B : Type}
 (* selectA x y = (\e f -> either f id e) <$> x <*> y *)
 Definition selectA `{Applicative f} {A B : Type}
            (x : f (Either A B)) (y : f (A -> B)) : f B :=
-  (fun e f => either f id e) <$> x <*> y. 
+  (fun e f => either f id e) <$> x <*> y.
 
 Module SelectiveLaws.
 
-Include ApplicativeLaws. 
+Include ApplicativeLaws.
 
 Definition law3_f {A B C : Type}
            (x : B + C) : B + (A + C) := Right <$> x.
@@ -62,4 +61,3 @@ Class SelectiveLaws (F : Type -> Type) `{Selective F} := {
 }.
 
 End SelectiveLaws.
-