From 75ed8394ea5747b3ad0c3d3b412a42a9c532d152 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Aug 2020 15:54:12 +0200
Subject: [PATCH] update for Coq 8.10 deprecations

---
 _CoqProject                       | 7 ++-----
 tests/proofmode_ascii.v           | 2 +-
 tests/proofmode_monpred.v         | 2 +-
 theories/algebra/cmra.v           | 2 ++
 theories/algebra/ofe.v            | 1 +
 theories/bi/monpred.v             | 1 +
 theories/bi/notation.v            | 1 +
 theories/heap_lang/notation.v     | 3 ---
 theories/program_logic/language.v | 6 +++++-
 theories/proofmode/environments.v | 2 +-
 theories/proofmode/ltac_tactics.v | 2 +-
 theories/proofmode/notation.v     | 1 +
 theories/proofmode/reduction.v    | 8 ++++----
 theories/si_logic/siprop.v        | 2 ++
 14 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index aeb000f4f..5a92de86d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,12 +2,9 @@
 # We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
 # is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
-# Non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294)
 -arg -w -arg -redundant-canonical-projection
-# change_no_check does not exist yet in 8.9.
--arg -w -arg -convert_concl_no_check
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
 
 theories/algebra/monoid.v
 theories/algebra/cmra.v
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index d1102210d..a05c9a716 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
 From iris.bi Require Import ascii.
 
 Set Default Proof Using "Type".
-Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
+Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
 
 Section base_logic_tests.
   Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 5d7b84d2a..f90d0db21 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
-Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
+Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
 
 Section tests.
   Context {I : biIndex} {PROP : bi}.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 979462cac..b56fade14 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -794,6 +794,7 @@ Record rFunctor := RFunctor {
 Existing Instances rFunctor_map_ne rFunctor_mor.
 Instance: Params (@rFunctor_map) 9 := {}.
 
+Declare Scope rFunctor_scope.
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
@@ -866,6 +867,7 @@ Record urFunctor := URFunctor {
 Existing Instances urFunctor_map_ne urFunctor_mor.
 Instance: Params (@urFunctor_map) 9 := {}.
 
+Declare Scope urFunctor_scope.
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 71c86a043..c96fc87bd 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -704,6 +704,7 @@ Record oFunctor := OFunctor {
 Existing Instance oFunctor_map_ne.
 Instance: Params (@oFunctor_map) 9 := {}.
 
+Declare Scope oFunctor_scope.
 Delimit Scope oFunctor_scope with OF.
 Bind Scope oFunctor_scope with oFunctor.
 
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index ee70c6117..6df3cd65d 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -26,6 +26,7 @@ Record monPred :=
             monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
 Local Existing Instance monPred_mono.
 
+Declare Scope monPred.
 Bind Scope monPred with bi.
 
 Implicit Types P Q : monPred.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 99599c3be..d67cc7f89 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -179,4 +179,5 @@ Reserved Notation "'[∗' 'mset]' x ∈ X , P"
    format "[∗  mset]  x  ∈  X ,  P").
 
 (** Define the scope *)
+Declare Scope bi_scope.
 Delimit Scope bi_scope with I.
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 0948a57f9..6e60bbd0a 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -2,9 +2,6 @@ From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang.
 Set Default Proof Using "Type".
 
-Delimit Scope expr_scope with E.
-Delimit Scope val_scope with V.
-
 (** Coercions to make programs easier to type. *)
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 2fa0f289e..6999e0163 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -27,9 +27,13 @@ Structure language := Language {
   prim_step : expr → state → list observation → expr → state → list expr → Prop;
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
+
+Declare Scope expr_scope.
 Delimit Scope expr_scope with E.
-Delimit Scope val_scope with V.
 Bind Scope expr_scope with expr.
+
+Declare Scope val_scope.
+Delimit Scope val_scope with V.
 Bind Scope val_scope with val.
 
 Arguments Language {_ _ _ _ _ _ _} _.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index e11fb4bce..5e99d04ed 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -234,7 +234,7 @@ an efficient way. Concretely, we made sure that [envs_entails (Envs Γp Γs c) Q
 and [envs_entails (Envs Γp Γs c') Q] are convertible for any [c] and [c']. This
 way, [iFresh] can simply be implemented by changing the goal from
 [envs_entails (Envs Γp Γs c) Q] into [envs_entails (Envs Γp Γs (Pos_succ c)) Q]
-using the tactic [convert_concl_no_check]. This way, the generated proof term
+using the tactic [change_no_check]. This way, the generated proof term
 contains no additional steps for changing the counter.
 
 For all definitions below, we first define a version that take the two contexts
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 1accdff03..203f53c92 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -123,7 +123,7 @@ Ltac iFresh :=
     lazymatch goal with
     | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
       let c' := eval vm_compute in (Pos.succ c) in
-      convert_concl_no_check (envs_entails (Envs Δp Δs c') Q)
+      change_no_check (envs_entails (Envs Δp Δs c') Q)
     end in
   constr:(IAnon c).
 
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index f9a53fb58..0025dc12e 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -2,6 +2,7 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import coq_tactics environments.
 Set Default Proof Using "Type".
 
+Declare Scope proof_scope.
 Delimit Scope proof_scope with env.
 Arguments Envs _ _%proof_scope _%proof_scope _.
 Arguments Enil {_}.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index b5af9b818..c9d616778 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -22,9 +22,9 @@ Declare Reduction pm_eval := cbv [
 Ltac pm_eval t :=
   eval pm_eval in t.
 Ltac pm_reduce :=
-  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  (* Use [change_no_check] instead of [change] to avoid performing the
   conversion check twice. *)
-  match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end.
+  match goal with |- ?u => let v := pm_eval u in change_no_check v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
 
 (** Called by many tactics for redexes that are created by instantiation.
@@ -38,6 +38,6 @@ Declare Reduction pm_prettify := cbn [
   bi_tforall bi_texist
 ].
 Ltac pm_prettify :=
-  (* Use [convert_concl_no_check] instead of [change] to avoid performing the
+  (* Use [change_no_check] instead of [change] to avoid performing the
   conversion check twice. *)
-  match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end.
+  match goal with |- ?u => let v := eval pm_prettify in u in change_no_check v end.
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index d1538b871..1ea1bde1f 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -10,6 +10,8 @@ Record siProp := SiProp {
 }.
 Arguments siProp_holds : simpl never.
 Add Printing Constructor siProp.
+
+Declare Scope siProp_scope.
 Delimit Scope siProp_scope with SI.
 Bind Scope siProp_scope with siProp.
 
-- 
GitLab