From ff575e3a9d9487fa566425d92de46d369b3663e7 Mon Sep 17 00:00:00 2001
From: Steven Keuchel <steven.keuchel@ugent.be>
Date: Thu, 8 May 2014 18:14:40 +0200
Subject: [PATCH] Use functor arguments instead of subfunctor instances.

Make the normal functor arguments of type Set -> Set of
Distinct_Sub_Functor explicit and make the Sub_Functor
instance arguments implicit instead.
---
 Arith.v        |  4 ++--
 Arith_Lambda.v |  4 ++--
 Bool.v         |  4 ++--
 Bool_Lambda.v  |  4 ++--
 Functors.v     | 22 +++++++++++-----------
 Lambda.v       |  2 +-
 NatCase.v      |  2 +-
 7 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/Arith.v b/Arith.v
index 0f61c2d..a308732 100644
--- a/Arith.v
+++ b/Arith.v
@@ -373,7 +373,7 @@ Section Arith.
 
   (* Add case. *)
 
-  Context {Dis_VI_Bot : Distinct_Sub_Functor _ Sub_NatValue_V Sub_BotValue_V}.
+  Context {Dis_VI_Bot : Distinct_Sub_Functor NatValue BotValue V}.
 
   (* Inversion principles for natural number SubValues. *)
   Definition SV_invertVI_P (i : SubValue_i V) :=
@@ -399,7 +399,7 @@ Section Arith.
     (WF_V' : WF_Functor V' V sub_V'_V),
     (forall (i : SubValue_i V) (H : SV' SV_invertVI_P i),
       exists v', proj1_sig (sv_a _ i) = inject v') ->
-    Distinct_Sub_Functor _ Sub_NatValue_V sub_V'_V ->
+    Distinct_Sub_Functor NatValue V' V ->
     iPAlgebra SV_invertVI_Name SV_invertVI_P SV'.
   Proof.
     econstructor; intros.
diff --git a/Arith_Lambda.v b/Arith_Lambda.v
index ae65ab5..9d46d2a 100644
--- a/Arith_Lambda.v
+++ b/Arith_Lambda.v
@@ -66,13 +66,13 @@ Section Lambda_Arith.
   Variable WFV : (WFValue_i D V -> Prop) -> WFValue_i D V -> Prop.
   Context {funWFV : iFunctor WFV}.
 
-  Context {Dis_VI_Clos : Distinct_Sub_Functor Fun_V Sub_NatValue_V Sub_ClosValue_V}.
+  Context {Dis_VI_Clos : Distinct_Sub_Functor NatValue (ClosValue E) V}.
   Context {WF_Sub_ClosValue_V : WF_Functor (ClosValue E) V Sub_ClosValue_V}.
   Context {WF_Sub_NatValue_V : WF_Functor NatValue V Sub_NatValue_V}.
 
   Context {Sub_WFV_VI_WFV : Sub_iFunctor (WFValue_VI D V) WFV}.
   Context {Sub_WFV_Bot_WFV : Sub_iFunctor (WFValue_Bot D V) WFV}.
-  Context {Dis_Clos_Bot : Distinct_Sub_Functor _ Sub_LType_D Sub_AType_D}.
+  Context {Dis_Clos_Bot : Distinct_Sub_Functor LType AType D}.
 
   Context {Typeof_E : forall T, FAlgebra TypeofName T (typeofR D) (E (typeofR D))}.
   Context {WF_typeof_E : forall T, @WF_FAlgebra TypeofName T _ _ _
diff --git a/Bool.v b/Bool.v
index 4f69c89..edf3f53 100644
--- a/Bool.v
+++ b/Bool.v
@@ -355,7 +355,7 @@ Section Bool.
   Context {SV : (SubValue_i V -> Prop) -> SubValue_i V -> Prop}.
   Context {Sub_SV_refl_SV : Sub_iFunctor (SubValue_refl V) SV}.
 
-  Context {Dis_VB_Bot : Distinct_Sub_Functor _ Sub_BoolValue_V Sub_BotValue_V}.
+  Context {Dis_VB_Bot : Distinct_Sub_Functor BoolValue BotValue V}.
 
   (* Inversion principles for natural number SubValues. *)
   Definition SV_invertVB_P (i : SubValue_i V) :=
@@ -381,7 +381,7 @@ Section Bool.
     (WF_V' : WF_Functor V' V sub_V'_V),
     (forall (i : SubValue_i V) (H : SV' SV_invertVB_P i),
       exists v', proj1_sig (sv_a _ i) = inject v') ->
-    Distinct_Sub_Functor _ Sub_BoolValue_V sub_V'_V ->
+    Distinct_Sub_Functor BoolValue V' V ->
     iPAlgebra SV_invertVB_Name SV_invertVB_P SV'.
   Proof.
     econstructor; intros.
diff --git a/Bool_Lambda.v b/Bool_Lambda.v
index d8ca026..11e3411 100644
--- a/Bool_Lambda.v
+++ b/Bool_Lambda.v
@@ -79,9 +79,9 @@ Section PLambda_Arith.
 
   Context {Sub_WFV_VB_WFV : Sub_iFunctor (WFValue_VB D V) WFV}.
   Context {Sub_WFV_Bot_WFV : Sub_iFunctor (WFValue_Bot D V) WFV}.
-  Context {Dis_Clos_Bot : Distinct_Sub_Functor _ Sub_LType_D Sub_BType_D}.
+  Context {Dis_Clos_Bot : Distinct_Sub_Functor LType BType D}.
 
-  Context {Dis_VB_Clos : Distinct_Sub_Functor Fun_V Sub_BoolValue_V Sub_ClosValue_V}.
+  Context {Dis_VB_Clos : Distinct_Sub_Functor BoolValue (ClosValue E) V}.
   Context {WF_Sub_ClosValue_V : WF_Functor (ClosValue E) V Sub_ClosValue_V}.
   Context {WF_Sub_BoolValue_V : WF_Functor BoolValue V Sub_BoolValue_V}.
 
diff --git a/Functors.v b/Functors.v
index b7249d2..6582bf8 100644
--- a/Functors.v
+++ b/Functors.v
@@ -494,10 +494,10 @@ Section Folds.
     reflexivity.
   Qed.
 
-  Class Distinct_Sub_Functor {F G H : Set -> Set}
-    (Fun_H : Functor H)
-    (sub_F_H : F :<: H)
-    (sub_G_H : G :<: H)
+  Class Distinct_Sub_Functor (F G H : Set -> Set)
+    {Fun_H : Functor H}
+    {sub_F_H : F :<: H}
+    {sub_G_H : G :<: H}
     : Set :=
     { inj_discriminate :
         forall A f g,
@@ -512,7 +512,7 @@ Section Folds.
     (sub_F_G : F :<: G)
     (sub_H_I : H :<: I)
     :
-    @Distinct_Sub_Functor F H (G :+: I) _ _ _.
+    Distinct_Sub_Functor F H (G :+: I).
   Proof.
     econstructor; intros.
     unfold not; simpl; unfold id; intros.
@@ -526,7 +526,7 @@ Section Folds.
     (sub_F_G : F :<: G)
     (sub_H_I : H :<: I)
     :
-    @Distinct_Sub_Functor F H (I :+: G) _ _ _.
+    Distinct_Sub_Functor F H (I :+: G).
   Proof.
     econstructor; intros.
     unfold not; simpl; unfold id; intros.
@@ -539,9 +539,9 @@ Section Folds.
     (Fun_I : Functor I)
     (sub_F_G : F :<: G)
     (sub_H_G : H :<: G)
-    (Dist_inl : @Distinct_Sub_Functor F H G Fun_G sub_F_G sub_H_G)
+    (Dist_inl : Distinct_Sub_Functor F H G)
     :
-    @Distinct_Sub_Functor F H (G :+: I) _ _ _.
+    Distinct_Sub_Functor F H (G :+: I).
   Proof.
     econstructor; intros.
     unfold not; intros.
@@ -555,9 +555,9 @@ Section Folds.
     (Fun_I : Functor I)
     (sub_F_G : F :<: G)
     (sub_H_G : H :<: G)
-    (Dist_inl : @Distinct_Sub_Functor F H G Fun_G sub_F_G sub_H_G)
+    (Dist_inl : Distinct_Sub_Functor F H G)
     :
-    @Distinct_Sub_Functor F H (I :+: G) _ _ _.
+    Distinct_Sub_Functor F H (I :+: G).
   Proof.
     econstructor; intros.
     unfold not; intros.
@@ -573,7 +573,7 @@ Section Folds.
     {sub_G_H : G :<: H}
     {WF_F : WF_Functor _ _ sub_F_H}
     {WF_G : WF_Functor _ _ sub_G_H},
-    Distinct_Sub_Functor Fun_H sub_F_H sub_G_H ->
+    Distinct_Sub_Functor F G H ->
     forall f g, inject (subGF := sub_F_H) f <> inject (subGF := sub_G_H) g.
   Proof.
     unfold inject; simpl; intros.
diff --git a/Lambda.v b/Lambda.v
index f44d750..aaf8882 100644
--- a/Lambda.v
+++ b/Lambda.v
@@ -545,7 +545,7 @@ Section Lambda.
 
   (* App case. *)
 
-  Context {Dis_Clos_Bot : Distinct_Sub_Functor _ Sub_ClosValue_V Sub_BotValue_V}.
+  Context {Dis_Clos_Bot : Distinct_Sub_Functor ClosValue BotValue V}.
   Context {iFun_SV : iFunctor SV}.
 
   Global Instance SV_proj1_b_Clos :
diff --git a/NatCase.v b/NatCase.v
index 46d89b4..794ba9b 100644
--- a/NatCase.v
+++ b/NatCase.v
@@ -186,7 +186,7 @@ Section NatCase.
     iPAlgebra SV_invertVI_Name (SV_invertVI_P V) SV}.
   Context {SV_invertVI'_SV :
     iPAlgebra SV_invertVI'_Name (SV_invertVI'_P V) SV}.
-  Context {Dis_VI_Bot : Distinct_Sub_Functor _ Sub_NatValue_V Sub_BotValue_V}.
+  Context {Dis_VI_Bot : Distinct_Sub_Functor NatValue BotValue V}.
   Context {SV_invertBot_SV :
     iPAlgebra SV_invertBot_Name (SV_invertBot_P V) SV}.