From 1bada58baa0739da1c37e0de949fdcf74e309eaa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Wed, 29 Jun 2022 11:05:52 +0200
Subject: [PATCH 1/2] Adapt w.r.t. coq/coq#16004.

---
 examples/StateTMonad.v           | 2 +-
 theories/Core/Any.v              | 1 +
 theories/Data/Eq.v               | 8 ++++++++
 theories/Data/ListFirstnSkipn.v  | 5 +++++
 theories/Data/Option.v           | 4 ++++
 theories/Data/PList.v            | 1 +
 theories/Data/POption.v          | 2 ++
 theories/Data/SigT.v             | 4 ++++
 theories/Generic/Ind.v           | 2 ++
 theories/Programming/Eqv.v       | 1 +
 theories/Programming/Injection.v | 3 +++
 theories/Programming/Le.v        | 3 +++
 theories/Tactics/BoolTac.v       | 6 +++++-
 theories/Tactics/Consider.v      | 1 +
 14 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/examples/StateTMonad.v b/examples/StateTMonad.v
index fb8081a2..11b905b1 100644
--- a/examples/StateTMonad.v
+++ b/examples/StateTMonad.v
@@ -8,7 +8,7 @@ Fail Definition foo : stateT unit option unit :=
   ret tt.
 
 (** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *)
-Existing Instance Monad_stateT.
+#[global] Existing Instance Monad_stateT.
 
 (** Now the definition succeeds *)
 Definition foo : stateT unit option unit :=
diff --git a/theories/Core/Any.v b/theories/Core/Any.v
index 299120b4..9cc0fed4 100644
--- a/theories/Core/Any.v
+++ b/theories/Core/Any.v
@@ -10,4 +10,5 @@ Polymorphic Definition RESOLVE (T : Type) : Type := T.
 
 Existing Class RESOLVE.
 
+#[global]
 Hint Extern 0 (RESOLVE _) => unfold RESOLVE : typeclass_instances.
diff --git a/theories/Data/Eq.v b/theories/Data/Eq.v
index 2dae4fe3..998d40f3 100644
--- a/theories/Data/Eq.v
+++ b/theories/Data/Eq.v
@@ -4,6 +4,9 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Create HintDb eq_rw discriminated.
 
 Lemma eq_sym_eq
@@ -28,6 +31,7 @@ Lemma match_eq_sym_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite match_eq_sym_eq : eq_rw.
 
 Lemma match_eq_sym_eq'
@@ -40,6 +44,7 @@ Lemma match_eq_sym_eq'
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite match_eq_sym_eq' : eq_rw.
 
 
@@ -73,6 +78,7 @@ Lemma eq_Const_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite eq_Const_eq : eq_rw.
 
 Lemma eq_Arr_eq
@@ -88,11 +94,13 @@ Lemma eq_Arr_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite eq_Arr_eq : eq_rw.
 
 Lemma eq_sym_eq_sym : forall (T : Type) (a b : T) (pf : a = b),
                         eq_sym (eq_sym pf) = pf.
 Proof. destruct pf. reflexivity. Defined.
+#[global]
 Hint Rewrite eq_sym_eq_sym : eq_rw.
 
 Ltac autorewrite_eq_rw :=
diff --git a/theories/Data/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
index ad5e284c..33d95cc8 100644
--- a/theories/Data/ListFirstnSkipn.v
+++ b/theories/Data/ListFirstnSkipn.v
@@ -2,6 +2,9 @@ Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Lemma firstn_app_L : forall T n (a b : list T),
   n <= length a ->
   firstn n (a ++ b) = firstn n a.
@@ -45,6 +48,7 @@ Proof.
   simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
+#[global]
 Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using lia : list_rw.
 
 Lemma skipn_app_R : forall T n (a b : list T),
@@ -90,4 +94,5 @@ Proof.
   simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
+#[global]
 Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using lia : list_rw.
diff --git a/theories/Data/Option.v b/theories/Data/Option.v
index 153c9b17..d375a42d 100644
--- a/theories/Data/Option.v
+++ b/theories/Data/Option.v
@@ -14,6 +14,9 @@ Require Import ExtLib.Tactics.Consider.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Global Instance Foldable_option {T} : Foldable (option T) T :=
   fun _ f d v =>
     match v with
@@ -180,4 +183,5 @@ Proof.
   destruct pf. destruct val; reflexivity.
 Defined.
 
+#[global]
 Hint Rewrite eq_option_eq : eq_rw.
diff --git a/theories/Data/PList.v b/theories/Data/PList.v
index b80dedfe..d8b9ff1f 100644
--- a/theories/Data/PList.v
+++ b/theories/Data/PList.v
@@ -216,6 +216,7 @@ End pmap.
 
 Polymorphic Definition Functor_plist@{i} : Functor@{i i} plist@{i} :=
 {| fmap := @fmap_plist@{i i} |}.
+#[global]
 Existing Instance Functor_plist.
 
 
diff --git a/theories/Data/POption.v b/theories/Data/POption.v
index 928f6463..ce2de987 100644
--- a/theories/Data/POption.v
+++ b/theories/Data/POption.v
@@ -80,9 +80,11 @@ End poption_map.
 
 Definition Functor_poption@{i} : Functor@{i i} poption@{i} :=
 {| fmap := @fmap_poption@{i i} |}.
+#[global]
 Existing Instance Functor_poption.
 
 Definition Applicative_poption@{i} : Applicative@{i i} poption@{i} :=
 {| pure := @pSome@{i}
  ; ap   := @ap_poption |}.
+#[global]
 Existing Instance Applicative_poption.
diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
index f452367f..0e964658 100644
--- a/theories/Data/SigT.v
+++ b/theories/Data/SigT.v
@@ -7,6 +7,9 @@ Set Implicit Arguments.
 Set Strict Implicit.
 Set Printing Universes.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Section injective.
   Variable T : Type.
   Variable F : T -> Type.
@@ -39,4 +42,5 @@ Lemma eq_sigT_rw
             end.
 Proof. destruct pf. destruct s; reflexivity. Qed.
 
+#[global]
 Hint Rewrite eq_sigT_rw : eq_rw.
diff --git a/theories/Generic/Ind.v b/theories/Generic/Ind.v
index 9c3763e4..2c2c6200 100644
--- a/theories/Generic/Ind.v
+++ b/theories/Generic/Ind.v
@@ -132,7 +132,9 @@ Ltac all_resolve :=
              | |- _ => solve [ eauto with typeclass_instances ]
            end.
 
+#[global]
 Hint Extern 0 (ProductResolve _ _) => all_resolve : typeclass_instances.
+#[global]
 Hint Extern 0 (VariantResolve _ _) => all_resolve : typeclass_instances.
 
 Definition comma_before (b : bool) (s : showM) : showM :=
diff --git a/theories/Programming/Eqv.v b/theories/Programming/Eqv.v
index 35547624..8bcd804a 100644
--- a/theories/Programming/Eqv.v
+++ b/theories/Programming/Eqv.v
@@ -9,6 +9,7 @@ Class EqvWF T :=
 { eqvWFEqv :> Eqv T
 ; eqvWFEquivalence :> Equivalence eqv
 }.
+#[global]
 Instance EqvWF_Build {T} {E:Eqv T} {EV:Equivalence eqv} : EqvWF T :=
   { eqvWFEqv := E ; eqvWFEquivalence := EV }.
 
diff --git a/theories/Programming/Injection.v b/theories/Programming/Injection.v
index 781e6953..14747c0d 100644
--- a/theories/Programming/Injection.v
+++ b/theories/Programming/Injection.v
@@ -9,10 +9,13 @@ Polymorphic Class Injection (x : Type) (t : Type) := inject : x -> t.
 Class Projection x t := { project : t -> x ; pmodify : (x -> x) -> (t -> t) }.
 *)
 
+#[global]
 Polymorphic Instance Injection_refl {T : Type} : Injection T T :=
 { inject := @id T }.
 
+#[global]
 Instance Injection_ascii_string : Injection ascii string :=
   { inject a := String a EmptyString }.
+#[global]
 Instance Injection_ascii_string_cons : Injection ascii (string -> string) :=
   { inject := String }.
diff --git a/theories/Programming/Le.v b/theories/Programming/Le.v
index 22231269..017fe04d 100644
--- a/theories/Programming/Le.v
+++ b/theories/Programming/Le.v
@@ -8,9 +8,11 @@ Definition neg_lte {T} {L:Lte T} (x:T) (y:T) : Prop := not (lte x y).
 Definition lt {T} {L:Lte T} x y := lte x y /\ ~lte y x.
 Definition neg_lt {T} {L:Lte T} x y := not (lt x y).
 
+#[global]
 Instance lt_RelDec {T} {L:Lte T} {RD:RelDec lte} : RelDec lt :=
   { rel_dec x y := (rel_dec x y && negb (rel_dec y x))%bool }.
 
+#[global]
 Instance lt_RelDecCorrect {T} {L:Lte T} {RD:RelDec lte} {RDC:RelDec_Correct RD}
   : RelDec_Correct lt_RelDec.
 Proof. constructor.
@@ -29,6 +31,7 @@ Class LteWF T :=
 ; lteWFPreOrder :> PreOrder lte
 }.
 
+#[global]
 Instance LteWF_Build {T} {L:Lte T} {PO:PreOrder lte} : LteWF T :=
   { lteWFLte := L ; lteWFPreOrder := PO }.
 
diff --git a/theories/Tactics/BoolTac.v b/theories/Tactics/BoolTac.v
index 06f46439..2e2a25d5 100644
--- a/theories/Tactics/BoolTac.v
+++ b/theories/Tactics/BoolTac.v
@@ -3,6 +3,10 @@ Require Import Coq.Bool.Bool.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
+#[global]
 Hint Rewrite negb_orb negb_andb negb_involutive if_negb : bool_rw.
 
 Lemma negb_true : forall a, negb a = true -> a = false.
@@ -56,4 +60,4 @@ Proof.
   intros.
   do_bool.
 Abort.
-*)
\ No newline at end of file
+*)
diff --git a/theories/Tactics/Consider.v b/theories/Tactics/Consider.v
index 72b40fd0..8023752a 100644
--- a/theories/Tactics/Consider.v
+++ b/theories/Tactics/Consider.v
@@ -101,6 +101,7 @@ Section from_rel_dec.
   Qed.
 End from_rel_dec.
 
+#[global]
 Hint Extern 10 (@Reflect (?f ?a ?b) _ _) =>
   eapply (@Reflect_RelDecCorrect _ _ (@Build_RelDec _ _ f) _) : typeclass_instances.
 

From ca799c7da41c7e92c291c53e028047ca61a9bf16 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Thu, 30 Jun 2022 20:42:29 -0400
Subject: [PATCH 2/2] Retire Coq 8.10

---
 .circleci/config.yml | 33 ++++++++++++---------------------
 meta.yml             | 15 ++++++---------
 2 files changed, 18 insertions(+), 30 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index f6b83502..a2f500f5 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -61,29 +61,20 @@ workflows:
   test:
     jobs:
     - build:
-        name: "Coq 8.8"
-        coq: "coqorg/coq:8.8"
+        name: "Coq 8.11"
+        coq: "coqorg/coq:8.11"
     - build:
-        name: "Coq 8.9"
-        coq: "coqorg/coq:8.9"
+        name: "Coq 8.12"
+        coq: "coqorg/coq:8.12"
     - build:
-        name: "Coq 8.10"
-        coq: "coqorg/coq:8.10"
+        name: "Coq 8.13"
+        coq: "coqorg/coq:8.13"
     - build:
-        name: "Coq 8.11-ocaml-4.11-flambda"
-        coq: "coqorg/coq:8.11-ocaml-4.11-flambda"
+        name: "Coq 8.14"
+        coq: "coqorg/coq:8.14"
     - build:
-        name: "Coq 8.12-ocaml-4.11-flambda"
-        coq: "coqorg/coq:8.12-ocaml-4.11-flambda"
+        name: "Coq 8.15"
+        coq: "coqorg/coq:8.15"
     - build:
-        name: "Coq 8.13-ocaml-4.12-flambda"
-        coq: "coqorg/coq:8.13-ocaml-4.12-flambda"
-    - build:
-        name: "Coq 8.14-ocaml-4.12-flambda"
-        coq: "coqorg/coq:8.14-ocaml-4.12-flambda"
-    - build:
-        name: "Coq 8.15-ocaml-4.12-flambda"
-        coq: "coqorg/coq:8.15-ocaml-4.12-flambda"
-    - build:
-        name: "Coq dev-ocaml-4.12-flambda"
-        coq: "coqorg/coq:dev-ocaml-4.12-flambda"
+        name: "Coq dev"
+        coq: "coqorg/coq:dev"
diff --git a/meta.yml b/meta.yml
index 13a49e04..81fc2bbc 100644
--- a/meta.yml
+++ b/meta.yml
@@ -32,15 +32,12 @@ supported_coq_versions:
   opam: '{ >= "8.8" }'
 
 tested_coq_opam_versions:
-  - version: '8.8'
-  - version: '8.9'
-  - version: '8.10'
-  - version: '8.11-ocaml-4.11-flambda'
-  - version: '8.12-ocaml-4.11-flambda'
-  - version: '8.13-ocaml-4.12-flambda'
-  - version: '8.14-ocaml-4.12-flambda'
-  - version: '8.15-ocaml-4.12-flambda'
-  - version: 'dev-ocaml-4.12-flambda'
+  - version: '8.11'
+  - version: '8.12'
+  - version: '8.13'
+  - version: '8.14'
+  - version: '8.15'
+  - version: 'dev'
 
 make_target: theories
 test_target: examples