Compatibility with Coq 8.11

Author: wkolowski

.gitignore

@@ -1,10 +1,14 @@
 *vo
+*vos
+*vok
 *glob
-*~
 *aux
+
 *crashcoqide
 *v.d
+
 makefile
 _CoqProject
+
 .*
-Awodey*
+*~

Base.v

@@ -221,13 +221,15 @@ match goal with
     | _ => my_simpl; eauto
 end.
 
+#[refine]
 Instance Setoid_kernel {A B : Type} (f : A -> B) : Setoid A :=
     {| equiv := fun a a' : A => f a = f a' |}.
 Proof. solve_equiv. Defined.
 
+#[refine]
 Instance Setoid_kernel_equiv {A B : Type} (S : Setoid B) (f : A -> B)
     : Setoid A := {| equiv := fun a a' : A => f a == f a' |}.
-Proof. solve_equiv. Defined.
+Proof. all: solve_equiv. Defined.
 
 Inductive JMequiv {A : Type} {is_setoid : Setoid A} (x : A)
     : forall {B : Type}, B -> Prop :=

Bifunctor.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Import Cat.Cat.
 
 Require Import Cat.Limits.BinProdCoprod.
@@ -31,6 +29,7 @@ Definition second
   {C D E : Cat} {F : Bifunctor C D E} {A : Ob C} {X Y : Ob D} (f : Hom X Y)
   : Hom (biob A X) (biob A Y) := bimap (id A) f.
 
+#[refine]
 Instance ProductBifunctor {C : Cat} {hp : has_products C} :
     Bifunctor C C C :=
 {
@@ -43,6 +42,7 @@ Proof.
   unfold Proper, respectful. all: fpair.
 Defined.
 
+#[refine]
 Instance CoproductBifunctor {C : Cat} {hp : has_coproducts C} :
     Bifunctor C C C :=
 {
@@ -54,6 +54,7 @@ Proof.
   unfold Proper, respectful. all: copair.
 Defined.
 
+#[refine]
 Instance BiComp {C C' D D' E : Cat}
     (B : Bifunctor C' D' E) (F : Functor C C') (G : Functor D D')
     : Bifunctor C D E :=
@@ -68,6 +69,7 @@ Proof.
   intros. rewrite 2 pres_id, bimap_pres_id. reflexivity.
 Defined.
 
+#[refine]
 Instance Const {E : Cat} (X : Ob E) (C D : Cat)
     : Bifunctor C D E :=
 {

CartesianClosed.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Export Cat.
 Require Import Limits.InitTerm.
 Require Import Limits.BinProdCoprod.

Cat.v

@@ -1,9 +1,5 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Export Cat.Base.
 
-(*Require Import Unicode.Utf8.*)
-
 Class Cat : Type :=
 {
     Ob : Type;
@@ -185,6 +181,7 @@ match goal with
     | _ => cbn in *
 end; eauto).
 
+#[refine]
 Instance Dual (C : Cat) : Cat :=
 {|
     Ob := Ob C;

Contravariant.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Import Cat.Cat.
 
 Set Implicit Arguments.
@@ -18,6 +16,7 @@ Class Contravariant (C : Cat) (D : Cat) : Type :=
 Arguments coob [C D] _ _.
 Arguments comap [C D] _ [X Y] _.
 
+#[refine]
 Instance Const {D : Cat} (X : Ob D) (C : Cat)
     : Contravariant C D :=
 {

Distributive.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Import BinProdCoprod.
 Require Import InitTerm.
 

Enriched.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Import Cat.Cat.
 Require Import Cat.Bifunctor.
 
@@ -37,6 +35,7 @@ Instance wut (C : Cat) (X Y : Ob C) : Setoid' :=
     setoid := @HomSetoid C X Y;
 }.
 
+#[refine]
 Instance Enriched_CoqSetoid : Enriched
   (Monoidal_has_terminal_and_products
     CoqSetoid_has_term

Exponential.v

@@ -22,9 +22,9 @@ Class has_exponentials (C : Cat) {hp : has_products C} : Type :=
       exponential_skolem X Y (expOb X Y) (eval X Y) (@curry X Y)
 }.
 
-Arguments expOb [C] [hp] [has_exponentials] _ _.
-Arguments eval [C] [hp] [has_exponentials] [X] [Y].
-Arguments curry [C] [hp] [has_exponentials] [X] [Y] [Z] _.
+Arguments expOb {C hp has_exponentials} _ _.
+Arguments eval  {C hp has_exponentials X Y}.
+Arguments curry {C hp has_exponentials X Y Z} _.
 
 Definition uncurry
     {C : Cat} {hp : has_products C} {he : has_exponentials C}
@@ -146,7 +146,7 @@ Proof.
       apply ProductFunctor_fmap_Proper; cat. rewrite H3; cat.
 Qed.
 
-Arguments exponential_skolem_uiso [C hp X Y E eval curry E' eval' curry'] _ _.
+Arguments exponential_skolem_uiso {C hp X Y E eval curry E' eval' curry'} _ _.
 
 Theorem exponential_skolem_iso :
   forall (C : Cat) (hp : has_products C) (X Y : Ob C)
@@ -172,6 +172,7 @@ Proof.
   cat.
 Qed.
 
+#[refine]
 Instance ExponentialFunctor
   (C : Cat) (hp : has_products C) (he : has_exponentials C)
   (X : Ob C) : Functor C C :=

Functor.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Import Cat.Cat.
 
 Set Implicit Arguments.
@@ -92,6 +90,7 @@ Proof.
     (* TODO : cat should work here *)
 Defined.
 
+#[refine]
 Instance FunctorComp {C D E : Cat} (T : Functor C D) (S : Functor D E)
     : Functor C E :=
 {
@@ -103,6 +102,7 @@ Proof.
   (* Functor laws *) all: functor.
 Defined.
 
+#[refine]
 Instance FunctorId (C : Cat) : Functor C C :=
 {
     fob := fun A : Ob C => A;
@@ -113,6 +113,7 @@ Proof.
   (* Functors laws *) all: functor.
 Defined.
 
+#[refine]
 Instance CAT : Cat :=
 {
     Ob := Cat;
@@ -129,6 +130,7 @@ Proof.
   (* Category laws *) all: cat.
 Defined.
 
+#[refine]
 Instance ConstFunctor {D : Cat} (X : Ob D) (C : Cat)
     : Functor C D :=
 {

Instances/Apartoid.v

@@ -1,5 +1,3 @@
-Add Rec LoadPath "/home/zeimer/Code/Coq".
-
 Require Import Cat.
 Require Import InitTerm.
 Require Import BinProdCoprod.
@@ -114,6 +112,7 @@ Proof.
   intros. intro. apply H0. apply H. apply H1.
 Qed.
 
+#[refine]
 Instance ApartoidCat : Cat :=
 {
     Ob := Apartoid;
@@ -137,6 +136,7 @@ Proof.
   (* Category laws *) all: apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_init : Apartoid :=
 {
     carrier := Empty_set;
@@ -149,6 +149,7 @@ Proof.
   red. exists (fun (e : Empty_set) => match e with end). apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_has_init : has_init ApartoidCat :=
 {
     init := Apartoid_init;
@@ -157,6 +158,7 @@ Instance Apartoid_has_init : has_init ApartoidCat :=
 Proof. apartoid. Defined.
 
 (* Things can be done this way too. *)
+#[refine]
 Instance Apartoid_has_init' : has_init ApartoidCat := {}.
 Proof.
   refine {| carrier := Empty_set;
@@ -170,6 +172,7 @@ Restart.
   all: apartoid'. exists (fun e : Empty_set => match e with end). apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_term : Apartoid :=
 {
     carrier := unit;
@@ -182,13 +185,15 @@ Proof.
   red; simpl. exists (fun _ => tt). auto.
 Defined.
 
+#[refine]
 Instance Apartoid_has_term : has_term ApartoidCat :=
 {
     term := Apartoid_term;
     delete := Apartoid_delete
 }.
 Proof. apartoid. Defined.
 
+#[refine]
 Instance Apartoid_prodOb (X Y : Apartoid) : Apartoid :=
 {
     carrier := prod X Y;
@@ -221,6 +226,7 @@ Proof.
   red. exists (fun x : X => (f x, g x)). apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_has_products : has_products ApartoidCat :=
 {
     prodOb := Apartoid_prodOb;
@@ -233,6 +239,7 @@ Proof.
   (* Product law *) apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_coprodOb (X Y : Apartoid) : Apartoid :=
 {
     carrier := X + Y;
@@ -275,6 +282,7 @@ Proof.
   destruct x, x'; apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_has_coproducts : has_coproducts ApartoidCat :=
 {
     coprodOb := Apartoid_coprodOb;
@@ -287,6 +295,7 @@ Proof.
   (* Product law *) red; apartoid'. destruct x; apartoid.
 Defined.
 
+#[refine]
 Instance Apartoid_bigProdOb {J : Set} (A : J -> Apartoid) : Apartoid :=
 {
     carrier := forall j : J, A j;
@@ -317,6 +326,7 @@ Proof.
   eapply Hfj; eauto.
 Defined.
 
+#[refine]
 Instance Apartoid_has_all_products : has_all_products ApartoidCat :=
 {
     bigProdOb := @Apartoid_bigProdOb;
@@ -332,6 +342,7 @@ Proof.
   eapply H; eauto.
 Defined.
 
+#[refine]
 Instance Apartoid_eq_ob {X Y : Apartoid} (f g : ApartoidHom X Y)
     : Apartoid :=
 {
@@ -406,6 +417,7 @@ Inductive Apartoid_coeq_equiv {X Y : Apartoid} (f g : ApartoidHom X Y)
         Apartoid_coeq_equiv f g y1 y3.
 
 (* TODO: finish *)
+#[refine]
 Instance Apartoid_coeq_ob {X Y : Apartoid} (f g : ApartoidHom X Y)
     : Apartoid :=
 {
@@ -428,6 +440,7 @@ Proof.
 
 (* TODO: make this more dependent (change JMeq to some lifted heterogenous
    apartness... *)
+#[refine]
 Instance Apartoid_bigCoprodOb {J : Apartoid} (A : J -> Apartoid) : Apartoid :=
 {
     carrier := {j : J & A j};