Merge pull request #32 from haselwarter/coq-8.17-compat

bump compatible Coq version to 8.18~

.github/workflows/docker-action.yml

@@ -18,17 +18,22 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-autosubst-ci.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

coq-autosubst.opam

@@ -23,7 +23,7 @@ substitutions."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.16~") | (= "dev")}
+  "coq" {(>= "8.14" & < "8.18~") | (= "dev")}
 ]
 
 tags: [

examples/plain/Decidable.v

@@ -7,10 +7,10 @@ Arguments decide X {_}.
 
 Ltac gen_Dec_eq := unfold Dec; unfold dec; decide equality.
 
-Instance decide_eq_nat (x y : nat) : Dec (x = y). gen_Dec_eq. Defined.
+Global Instance decide_eq_nat (x y : nat) : Dec (x = y). gen_Dec_eq. Defined.
 
-Instance decide_le_nat (x y : nat) : Dec (x <= y). apply le_dec. Defined.
+Global Instance decide_le_nat (x y : nat) : Dec (x <= y). apply le_dec. Defined.
 
-Instance decide_lt_nat (x y : nat) : Dec (x < y). apply lt_dec. Defined.
+Global Instance decide_lt_nat (x y : nat) : Dec (x < y). apply lt_dec. Defined.
 
-Tactic Notation "decide" constr(p) := destruct (decide p).
+Tactic Notation "decide" constr(p) := destruct (decide p).

examples/plain/Demo.v

@@ -38,10 +38,10 @@ Inductive term :=
 
     Each instance is inferred automatically by using the [derive] tactic. *)
 
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (** At this point we can use the notations:
 

examples/plain/POPLmark.v

@@ -15,13 +15,13 @@ Inductive type : Type :=
 | Arr (A1 A2 : type)
 | All (A1 : type) (A2 : {bind type}).
 
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
+Global Instance Ids_type : Ids type. derive. Defined.
+Global Instance Rename_type : Rename type. derive. Defined.
+Global Instance Subst_type : Subst type. derive. Defined.
 
-Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
+Global Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
 
-Instance size_type : Size type.
+Global Instance size_type : Size type.
   assert(Size var). exact(fun _ => 0). derive.
 Defined.
 
@@ -32,19 +32,19 @@ Inductive term :=
 | TAbs (A : type) (s : {bind type in term})
 | TApp (s : term) (A : type).
 
-Instance hsubst_term : HSubst type term. derive. Defined.
+Global Instance hsubst_term : HSubst type term. derive. Defined.
 
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
 
-Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
+Global Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
 
-Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
+Global Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
 
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
-Instance size_term : Size term.
+Global Instance size_term : Size term.
   assert(Size var). exact(fun _ => 0). derive.
 Defined.
 

examples/plain/Size.v

@@ -31,7 +31,7 @@ Ltac derive_Size :=
     end
   end.
 
-Hint Extern 0 (Size _) => derive_Size : derive.
+Global Hint Extern 0 (Size _) => derive_Size : derive.
 
 Lemma size_rec {A : Type} f (x : A) :
   forall P : A -> Type, (forall x, (forall y, f y < f x -> P y) -> P x) -> P x.
@@ -78,11 +78,11 @@ Ltac sizesimpl := repeat(simpl in *;
 
 Tactic Notation "slia" := sizesimpl; try lia; now trivial.
 
-Instance size_list (A : Type) (size_A : Size A) : Size (list A).
+Global Instance size_list (A : Type) (size_A : Size A) : Size (list A).
   derive.
 Defined.
 
-Instance size_nat : Size nat := id.
+Global Instance size_nat : Size nat := id.
 
 (** A database of facts about the size function *)
 
@@ -93,9 +93,9 @@ Arguments size_fact {A} x {P _}.
 Lemma size_app (A : Type) (size_A : Size A) l1 l2 :
   size (app l1 l2) = size l1 + size l2.
 Proof. induction l1; simpl; intuition. Qed.
-Hint Rewrite @size_app : size.
+Global Hint Rewrite @size_app : size.
 
-Instance size_fact_app (A : Type) (size_A : Size A) l1 l2 :
+Global Instance size_fact_app (A : Type) (size_A : Size A) l1 l2 :
   SizeFact _ (app l1 l2) (size(app l1 l2) = size l1 + size l2).
 Proof. apply size_app. Qed.
 
@@ -107,7 +107,7 @@ Proof.
   - pose (IHl _ H0). lia.
 Qed.
 
-Instance size_fact_In (A : Type) (size_A : Size A) x l (x_in_l : In x l) :
+Global Instance size_fact_In (A : Type) (size_A : Size A) x l (x_in_l : In x l) :
   SizeFact _ x (size x < size l).
 Proof. now apply size_In. Qed.
 

examples/ssr/ARS.v

@@ -41,7 +41,7 @@ Definition diamond := forall x y z, e x y -> e x z -> exists2 u, e y u & e z u.
 Definition confluent := forall x y z, star x y -> star x z -> joinable star y z.
 Definition CR := forall x y, conv x y -> joinable star x y.
 
-Hint Resolve starR convR.
+Local Hint Resolve starR convR.
 
 Lemma star1 x y : e x y -> star x y.
 Proof. exact: starSE. Qed.
@@ -92,7 +92,7 @@ Qed.
 
 End Definitions.
 
-Hint Resolve starR convR.
+Global Hint Resolve starR convR.
 Arguments star_trans {T e} y {x z} A B.
 Arguments conv_trans {T e} y {x z} A B.
 

examples/ssr/BetaSubstitution.v

@@ -12,10 +12,10 @@ Inductive term :=
 | App (s t : term)
 | Lam (s : {bind term}).
 
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (** The optimized implementation of single variable substitutions *)
 

examples/ssr/CR.v

@@ -13,10 +13,10 @@ Inductive term : Type :=
 | App (s t : term)
 | Lam (s : {bind term}).
 
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (** **** One-Step Reduction *)
 
@@ -57,7 +57,7 @@ Qed.
 Lemma red_lam s1 s2 : red s1 s2 -> red (Lam s1) (Lam s2).
 Proof. apply: star_hom => x y. exact: step_lam. Qed.
 
-Hint Resolve red_app red_lam : red_congr.
+Global Hint Resolve red_app red_lam : red_congr.
 
 (** **** Church-Rosser theorem *)
 
@@ -88,7 +88,7 @@ Proof. move<-. exact: pstep_beta. Qed.
 
 Lemma pstep_refl s : pstep s s.
 Proof. elim: s; eauto using pstep. Qed.
-Hint Resolve pstep_refl.
+Global Hint Resolve pstep_refl.
 
 Lemma step_pstep s t : step s t -> pstep s t.
 Proof. elim; eauto using pstep. Qed.

examples/ssr/POPLmark.v

@@ -29,17 +29,17 @@ Inductive term :=
 
 (** **** Substitutions *)
 
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
-Instance HSubst_term : HSubst type term. derive. Defined.
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
-Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
-Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance Ids_type : Ids type. derive. Defined.
+Global Instance Rename_type : Rename type. derive. Defined.
+Global Instance Subst_type : Subst type. derive. Defined.
+Global Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
+Global Instance HSubst_term : HSubst type term. derive. Defined.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
+Global Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
+Global Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (** **** Subtyping *)
 
@@ -66,7 +66,7 @@ where "'SUB' Gamma |- A <: B" := (sub Gamma A B).
 
 Lemma sub_refl Gamma A : SUB Gamma |- A <: A.
 Proof. elim: A Gamma; eauto using sub. Qed.
-Hint Resolve sub_refl.
+Global Hint Resolve sub_refl.
 
 Lemma sub_ren Gamma Delta xi A B :
   (forall x, x < size Gamma -> xi x < size Delta) ->
@@ -94,7 +94,7 @@ Lemma transitivity_proj Gamma A B C :
   transitivity_at B ->
   SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
 Proof. move=> /(_ Gamma A C id). autosubst. Qed.
-Hint Resolve transitivity_proj.
+Global Hint Resolve transitivity_proj.
 
 Lemma transitivity_ren B xi : transitivity_at B -> transitivity_at B.[ren xi].
 Proof. move=> h Gamma A C zeta. asimpl. exact: h. Qed.

examples/ssr/SystemF_CBV.v

@@ -23,22 +23,22 @@ Inductive term :=
 
 (** **** Substitution Lemmas *)
 
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
+Global Instance Ids_type : Ids type. derive. Defined.
+Global Instance Rename_type : Rename type. derive. Defined.
+Global Instance Subst_type : Subst type. derive. Defined.
 
-Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
+Global Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
 
-Instance HSubst_term : HSubst type term. derive. Defined.
+Global Instance HSubst_term : HSubst type term. derive. Defined.
 
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
 
-Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
-Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
+Global Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
+Global Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
 
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (** **** Call-by value reduction *)
 
@@ -51,7 +51,7 @@ Inductive eval : term -> term -> Prop :=
     eval (Abs A s) (Abs A s)
 | eval_tabs (A : term) :
     eval (TAbs A) (TAbs A).
-Hint Resolve eval_abs eval_tabs.
+Global Hint Resolve eval_abs eval_tabs.
 
 (** **** Syntactic typing *)
 
@@ -92,11 +92,11 @@ Notation E A rho := (L (V A rho)).
 
 Lemma V_value A rho v : V A rho v -> eval v v.
 Proof. by elim: A => [x[]|A _ B _/=[A'[s->]]|A _/=[s->]]. Qed.
-Hint Resolve V_value.
+Global Hint Resolve V_value.
 
 Lemma V_to_E A rho v : V A rho v -> E A rho v.
 Proof. exists v; eauto. Qed.
-Hint Resolve V_to_E.
+Global Hint Resolve V_to_E.
 
 Lemma eq_V A rho1 rho2 v :
   (forall X v, eval v v -> (rho1 X v <-> rho2 X v)) -> V A rho1 v -> V A rho2 v.

examples/ssr/SystemF_SN.v

@@ -24,22 +24,22 @@ Inductive term :=
 
 (** **** Substitution Lemmas *)
 
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
+Global Instance Ids_type : Ids type. derive. Defined.
+Global Instance Rename_type : Rename type. derive. Defined.
+Global Instance Subst_type : Subst type. derive. Defined.
 
-Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
+Global Instance SubstLemmas_type : SubstLemmas type. derive. Qed.
 
-Instance HSubst_term : HSubst type term. derive. Defined.
+Global Instance HSubst_term : HSubst type term. derive. Defined.
 
-Instance Ids_term : Ids term. derive. Defined.
-Instance Rename_term : Rename term. derive. Defined.
-Instance Subst_term : Subst term. derive. Defined.
+Global Instance Ids_term : Ids term. derive. Defined.
+Global Instance Rename_term : Rename term. derive. Defined.
+Global Instance Subst_term : Subst term. derive. Defined.
 
-Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
-Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
+Global Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
+Global Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.
 
-Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
+Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
 
 (** **** One-Step Reduction *)
 
@@ -116,7 +116,7 @@ Lemma sred_hup sigma tau theta :
   sred sigma tau -> sred (sigma >>| theta) (tau >>| theta).
 Proof. move=> A n /=. apply/red_hsubst/A. Qed.
 
-Hint Resolve red_app red_abs red_tapp red_tabs sred_up sred_hup : red_congr.
+Global Hint Resolve red_app red_abs red_tapp red_tabs sred_up sred_hup : red_congr.
 
 Lemma red_compat sigma tau s :
   sred sigma tau -> red s.[sigma] s.[tau].
@@ -198,7 +198,7 @@ Definition admissible (rho : nat -> cand) :=
 
 Lemma reducible_sn : reducible sn.
 Proof. constructor; eauto using ARS.sn. by move=> s t [f] /f. Qed.
-Hint Resolve reducible_sn.
+Global Hint Resolve reducible_sn.
 
 Lemma reducible_var P x : reducible P -> P (TeVar x).
 Proof. move/p_nc. apply=> // t st. inv st. Qed.