From 72a8f88592e341ab8c5f502c927cd30d3df81092 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Nov 2019 12:13:07 +0100
Subject: [PATCH] Fix compilation with Coq 8.10 and kill some warnings.

---
 _CoqProject                   |  2 ++
 theories/examples/various.v   | 12 ++++++------
 theories/logic/model.v        |  1 +
 theories/logic/spec_rules.v   | 10 +++++-----
 theories/typing/fundamental.v |  2 +-
 theories/typing/types.v       |  1 +
 6 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 5b36787..271fa04 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,8 @@
 -arg -w -arg -convert_concl_no_check
 # non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
 -arg -w -arg -redundant-canonical-projection
+# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
+-arg -w -arg -ambiguous-paths
 
 theories/prelude/ctx_subst.v
 theories/prelude/properness.v
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 09477ad..b884eb7 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -7,6 +7,12 @@ From iris.algebra Require Import csum agree excl.
 From reloc Require Export reloc.
 From reloc.lib Require Export lock counter Y.
 
+Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
+Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
+Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
+Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
+Proof. solve_inG. Qed.
+
 Section proofs.
   Context `{relocG Σ}.
 
@@ -35,12 +41,6 @@ Section proofs.
       rel_values.
   Qed.
 
-  Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
-  Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
-  Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
-  Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
-  Proof. solve_inG. Qed.
-
   Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
   Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
   Lemma new_pending `{oneshotG Σ} : (|==> ∃ γ, pending γ)%I.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 057ce90..ffa2377 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -18,6 +18,7 @@ Record lrel Σ := LRel {
 }.
 Arguments LRel {_} _%I {_}.
 Arguments lrel_car {_} _ _ _ : simpl never.
+Declare Scope lrel_scope.
 Bind Scope lrel_scope with lrel.
 Delimit Scope lrel_scope with lrel.
 Existing Instance lrel_persistent.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2849bfd..3b7be1f 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -14,11 +14,11 @@ Section rules.
   Implicit Types v : val.
   Implicit Types l : loc.
 
-  Local Hint Resolve tpool_lookup.
-  Local Hint Resolve tpool_lookup_Some.
-  Local Hint Resolve to_tpool_insert.
-  Local Hint Resolve to_tpool_insert'.
-  Local Hint Resolve tpool_singleton_included.
+  Local Hint Resolve tpool_lookup : core.
+  Local Hint Resolve tpool_lookup_Some : core.
+  Local Hint Resolve to_tpool_insert : core.
+  Local Hint Resolve to_tpool_insert' : core.
+  Local Hint Resolve tpool_singleton_included : core.
 
   (** * Aux. lemmas *)
   Lemma step_insert K tp j e σ κ e' σ' efs :
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 8622240..430ac9f 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -11,7 +11,7 @@ From Autosubst Require Import Autosubst.
 Section fundamental.
   Context `{relocG Σ}.
   Implicit Types Δ : listO (lrelC Σ).
-  Hint Resolve to_of_val.
+  Hint Resolve to_of_val : core.
 
   Local Ltac intro_clause := progress (iIntros (vs) "#Hvs /=").
   Local Ltac intro_clause' := progress (iIntros (?) "? /=").
diff --git a/theories/typing/types.v b/theories/typing/types.v
index ecc67ba..d5722e9 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -51,6 +51,7 @@ Fixpoint binop_bool_res_type (op : bin_op) : option type :=
   | _ => None
   end.
 
+Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
 Bind Scope FType_scope with type.
 Infix "*" := TProd : FType_scope.
-- 
GitLab