From 8004a1a60dc6c2b486f0a733f0cfc66a14656826 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 1 Nov 2018 12:34:13 +0100 Subject: [PATCH] fix Coq 8.9 deprecation warnings --- theories/algebra/cofe_solver.v | 2 +- theories/algebra/sts.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v index 0b473a792..010d4afe2 100644 --- a/theories/algebra/cofe_solver.v +++ b/theories/algebra/cofe_solver.v @@ -21,7 +21,7 @@ Notation map := (cFunctor_map F). Fixpoint A (k : nat) : ofeT := match k with 0 => unitC | S k => F (A k) end. Local Instance: ∀ k, Cofe (A k). -Proof using Fcofe. induction 0; apply _. Defined. +Proof using Fcofe. induction k; apply _. Defined. Fixpoint f (k : nat) : A k -n> A (S k) := match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end with g (k : nat) : A (S k) -n> A k := diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v index 4843e6f03..50c494b91 100644 --- a/theories/algebra/sts.v +++ b/theories/algebra/sts.v @@ -64,7 +64,7 @@ Qed. Global Instance frame_step_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step. Proof. move=> ?? /collection_equiv_spec [??]; split; by apply frame_step_mono. Qed. Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed. -Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed. +Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed. Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed. Proof. by split; apply closed_proper'. Qed. Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up. -- GitLab