Fixes for Coq8.4.

Fix the different handling of implicit parameters in the mfold, imfold, ifold_,
fmapLambda and fmapFix functions. Explicitly pass the functor parameter to
typeofR when it is guessed incorreclty and fix failing proof scripts.

Arith.v

@@ -1052,7 +1052,7 @@ Section Arith.
       exact (proj2_sig d0).
     Defined.
 
-    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR _) F}.
+    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D) F}.
     Context {WF_typeof_F : forall T, @WF_FAlgebra TypeofName T _ _ _
       Sub_Arith_F (MAlgebra_typeof_Arith T) (Typeof_F _)}.
     Context {WF_Value_continous_alg : 
@@ -1065,7 +1065,7 @@ Section Arith.
       {Fun_E' : Functor E'}
       {Sub_Arith_E' : Arith :<: E'}
       {WF_Fun_E' : WF_Functor _ _ Sub_Arith_E' _ _}
-      {Typeof_E' : forall T, FAlgebra TypeofName T (typeofR _) E'}
+      {Typeof_E' : forall T, FAlgebra TypeofName T (typeofR D) E'}
       {WF_typeof_E' : forall T, @WF_FAlgebra TypeofName T _ _ _
         Sub_Arith_E' (MAlgebra_typeof_Arith T) (Typeof_E' _)}
       (pb : P_bind)

Arith_Lambda.v

@@ -74,7 +74,7 @@ Section Lambda_Arith.
   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 {Typeof_E : forall T, FAlgebra TypeofName T (typeofR _) (E (typeofR _))}.
+  Context {Typeof_E : forall T, FAlgebra TypeofName T (typeofR D) (E (typeofR D))}.
   Context {WF_typeof_E : forall T, @WF_FAlgebra TypeofName T _ _ _
     (Sub_Arith_E _) (MAlgebra_typeof_Arith _ T) (Typeof_E _)}.
 

Bool.v

@@ -629,7 +629,7 @@ Section Bool.
       discriminate.
     Defined.
 
-    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR _) F}.
+    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D) F}.
     Context {WF_typeof_F : forall T, @WF_FAlgebra TypeofName T _ _ _
       Sub_Bool_F (MAlgebra_typeof_Bool T) (Typeof_F _)}.
     Context {WF_Value_continous_alg : 
@@ -642,7 +642,7 @@ Section Bool.
       {Fun_E' : Functor E'}
       {Sub_Bool_E' : Bool :<: E'}
       {WF_Fun_E' : WF_Functor _ _ Sub_Bool_E' _ _}
-      {Typeof_E' : forall T, FAlgebra TypeofName T (typeofR _) E'}
+      {Typeof_E' : forall T, FAlgebra TypeofName T (typeofR D) E'}
       {WF_typeof_E' : forall T, @WF_FAlgebra TypeofName T _ _ _
         Sub_Bool_E' (MAlgebra_typeof_Bool T) (Typeof_E' _)}
       (pb : P_bind)

Bool_Lambda.v

@@ -64,7 +64,7 @@ Section PLambda_Arith.
   Variable E : Set -> Set -> Set.
   Context {Fun_E : forall A, Functor (E A)}.
   Context {Sub_Bool_E : forall A, Bool :<: (E A)}.
-  Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR _) (E (typeofR _))}.
+  Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D) (E (typeofR D))}.
   Variable EQV_E : forall A B, (eqv_i E A B -> Prop) -> eqv_i E A B -> Prop.
   Context {funEQV_E : forall A B, iFunctor (EQV_E A B)}.
 

Functors.v

@@ -23,7 +23,7 @@ Section Folds.
    Definition Fix (F : Set -> Set) : Set := 
     forall (A : Set), MAlgebra F A -> A.
 
-  Definition mfold {F : Set -> Set} : forall {A : Set}
+  Definition mfold {F : Set -> Set} : forall (A : Set)
     (f : MAlgebra F A), Fix F -> A:= fun A f e => e A f.
 
   Class Functor (F : Set -> Set) :=
@@ -71,7 +71,7 @@ Section Folds.
     forall (A : I -> Prop), iMAlgebra F A -> A i.
 
   Definition imfold {I : Set} (F : (I -> Prop) -> I -> Prop) : 
-    forall {A : I -> Prop} (f : iMAlgebra F A) {i : I},
+    forall (A : I -> Prop) (f : iMAlgebra F A) (i : I),
       iFix F i -> A i := fun A f i e => e A f.
 
   Class iFunctor {I : Set} (F : (I -> Prop) -> I -> Prop) :=
@@ -89,7 +89,7 @@ Section Folds.
     fun i F_e A f => f _ _ (imfold _ _ f) F_e.
 
   Definition ifold_ {I : Set} (F : (I -> Prop) -> I -> Prop) {iFun_F : iFunctor F} : 
-    forall {A : I -> Prop} (f : iAlgebra F A) {i : I},
+    forall (A : I -> Prop) (f : iAlgebra F A) (i : I),
       iFix F i -> A i := fun A f i e => imfold _ _ (fun i' r rec fa => f i' (ifmap i' rec fa)) i e.
 
   Definition out_ti {I : Set} {F} {fun_F : iFunctor F} : forall i : I, iFix F i -> F (iFix F) i :=

Lambda.v

@@ -180,7 +180,7 @@ Section Lambda.
 
   (** Functor Instance **)
 
-  Definition fmapLambda {A} : forall {X Y: Set}, (X -> Y) -> (Lambda A X -> Lambda A Y):=
+  Definition fmapLambda {A} : forall (X Y: Set), (X -> Y) -> (Lambda A X -> Lambda A Y):=
     fun _ _ f e =>
       match e with
        | Var a      => Var _ _ a
@@ -633,8 +633,7 @@ Section Lambda.
       repeat rewrite out_in_inverse in H2.
       repeat rewrite wf_functor in H2; simpl in H2.
       apply (f_equal (prj (Sub_Functor := Sub_ClosValue_V))) in H2.
-      repeat rewrite prj_inj in H2; injection H2; intros; 
-        subst.
+      repeat rewrite prj_inj in H2.
       split; intros.
       apply (inject_i (subGF := Sub_SV_Clos_SV)); econstructor; eauto.
       eapply H1; reflexivity.
@@ -644,10 +643,10 @@ Section Lambda.
       exact (proj2_sig v).
       simpl; eauto.
       exists f'; exists env'; repeat split; eauto.
-      rewrite H5 in H4; rewrite out_in_inverse, wf_functor, prj_inj in H4;
-        simpl in H4; injection H4; intros; congruence.
-      rewrite H5 in H4; rewrite out_in_inverse, wf_functor, prj_inj in H4;
-        simpl in H4; injection H4; intros; subst; eauto.
+      rewrite H4 in H2; rewrite out_in_inverse, wf_functor, prj_inj in H2;
+        simpl in H4; injection H2; intros; congruence.
+      rewrite H4 in H2; rewrite out_in_inverse, wf_functor, prj_inj in H2;
+        simpl in H4; injection H2; intros; subst; eauto.
       destruct env''; try discriminate; constructor.
       unfold SV_invertClos_P in H0.
       destruct env''; try discriminate; injection H2; intros; subst; 
@@ -935,15 +934,15 @@ Section Lambda.
     Global Instance iFun_Lambda_eqv A B : iFunctor (Lambda_eqv A B).
       constructor 1 with (ifmap := Lambda_eqv_ifmap A B).
       destruct a; simpl; intros; reflexivity.
-      destruct a; simpl; intros; unfold id; eauto.
-      rewrite (functional_extensionality_dep _ a); eauto.
+      destruct a; simpl; intros; unfold id; eauto;
+      rewrite (functional_extensionality_dep _ a); eauto;
       intros; apply functional_extensionality_dep; eauto.
     Defined.
 
     Variable Sub_Lambda_eqv_EQV_E : forall A B, 
       Sub_iFunctor (Lambda_eqv A B) (EQV_E A B).
 
-    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR _) (F (typeofR _))}.
+    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D) (F (typeofR D))}.
 
      Global Instance EQV_proj1_Lambda_eqv : 
        forall A B, iPAlgebra EQV_proj1_Name (EQV_proj1_P F EQV_E A B) (Lambda_eqv _ _).

Mu.v

@@ -22,7 +22,7 @@ Section Mu.
 
   (** Functor Instance **)
 
-  Definition fmapFix {A} : forall {X Y: Set}, (X -> Y) -> (Fix_ A X -> Fix_ A Y):=
+  Definition fmapFix {A} : forall (X Y: Set), (X -> Y) -> (Fix_ A X -> Fix_ A Y):=
     fun _ _ f e =>
       match e with
        | Mu t g => Mu _ _ t (fun a => f (g a))
@@ -245,15 +245,15 @@ Section Mu.
     Global Instance iFun_Fix_eqv A B : iFunctor (Fix_eqv A B).
       constructor 1 with (ifmap := Fix_eqv_ifmap A B).
       destruct a; simpl; intros; reflexivity.
-      destruct a; simpl; intros; unfold id; eauto.
-      rewrite (functional_extensionality_dep _ a); eauto.
+      destruct a; simpl; intros; unfold id; eauto;
+      rewrite (functional_extensionality_dep _ a); eauto;
       intros; apply functional_extensionality_dep; eauto.
     Defined.
 
     Variable Sub_Fix_eqv_EQV_E : forall A B, 
       Sub_iFunctor (Fix_eqv A B) (EQV_E A B).
 
-    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR _) (F (typeofR _))}.
+    Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D) (F (typeofR D))}.
 
      Global Instance EQV_proj1_Fix_eqv : 
        forall A B, iPAlgebra EQV_proj1_Name (EQV_proj1_P F EQV_E A B) (Fix_eqv _ _).

NatCase.v

@@ -32,7 +32,7 @@ Section NatCase.
   Proof. 
     destruct a; reflexivity.
   (* fmap id *)
-    destruct a; unfold id; simpl; auto.
+    destruct a; unfold id; simpl; auto;
     rewrite <- eta_expansion_dep; reflexivity.
   Defined.  
 
@@ -223,7 +223,7 @@ Section NatCase.
       rewrite <- (P2_Env_length _ _ _ _ _ H1).
       repeat erewrite bF_UP_in_out.
       unfold Names.Exp, evalR.
-      unfold isVI; caseEq (project (proj1_sig (beval V (F _) n0 (exist _ _ n_UP) gamma'))).
+      unfold isVI; caseEq (project (G := NatValue) (proj1_sig (beval V (F _) n0 (exist _ _ n_UP) gamma'))).
       unfold beval, Names.Exp, evalR in H3; rewrite H3.
       destruct n1.
       apply project_inject in H3; auto with typeclass_instances; 
@@ -248,7 +248,7 @@ Section NatCase.
       rewrite project_vi_bot, project_bot_bot; eauto.
       apply inject_i; constructor; reflexivity.
       exact (proj2_sig _).
-      unfold isVI; caseEq (project (proj1_sig (beval V (F _) m (exist _ _ n_UP) gamma))).
+      unfold isVI; caseEq (project (G := NatValue) (proj1_sig (beval V (F _) m (exist _ _ n_UP) gamma))).
       unfold beval, Names.Exp, evalR in H5; rewrite H5.
       destruct n1.
       apply project_inject in H5; auto with typeclass_instances; 
@@ -333,8 +333,8 @@ Section NatCase.
     Global Instance iFun_NatCase_eqv A B : iFunctor (NatCase_eqv A B).
       constructor 1 with (ifmap := NatCase_eqv_ifmap A B).
       destruct a; simpl; intros; reflexivity.
-      destruct a; simpl; intros; unfold id; eauto.
-      rewrite (functional_extensionality_dep _ a1); eauto.
+      destruct a; simpl; intros; unfold id; eauto;
+      rewrite (functional_extensionality_dep _ a1); eauto;
       intros; apply functional_extensionality_dep; eauto.
     Defined.
 
@@ -399,7 +399,7 @@ Section NatCase.
   Context {WFV_proj1_b_WFV :
     iPAlgebra WFV_proj1_b_Name (WFV_proj1_b_P D V WFV) WFV}.
 
-  Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR _) (F (typeofR D))}.
+  Context {Typeof_F : forall T, FAlgebra TypeofName T (typeofR D) (F (typeofR D))}.
   Context {WF_typeof_F : forall T, @WF_FAlgebra TypeofName T _ _ _
     (Sub_NatCase_F _) (MAlgebra_typeof_NatCase _) (Typeof_F _)}.
   Context {eval_F' : FAlgebra EvalName (Exp nat) (evalR V) (F nat)}.
@@ -565,7 +565,5 @@ End NatCase.
 (*
 *** Local Variables: ***
 *** coq-prog-args: ("-emacs-U" "-impredicative-set") ***
-
-
 *** End: ***
 *)