From 2d6aa0bd4ef9674d4fc345f7bd5c347a57540d74 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 25 May 2019 13:25:36 +0200
Subject: [PATCH] logrel: fix for Coq master

---
 theories/logrel/F_mu/logrel.v                 |  2 +-
 theories/logrel/F_mu_ref_conc/examples/lock.v |  8 +++----
 .../F_mu_ref_conc/examples/stack/CG_stack.v   | 22 +++++++++----------
 .../F_mu_ref_conc/examples/stack/FG_stack.v   | 12 +++++-----
 4 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/theories/logrel/F_mu/logrel.v b/theories/logrel/F_mu/logrel.v
index 4c2450e1..ff721cbb 100644
--- a/theories/logrel/F_mu/logrel.v
+++ b/theories/logrel/F_mu/logrel.v
@@ -88,7 +88,7 @@ Section logrel.
     env_Persistent Δ → Persistent (ctx_lookup x Δ v).
   Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
   Global Instance interp_persistent τ Δ v :
-    env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v) := _.
+    env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v).
   Proof.
     revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _.
     rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
diff --git a/theories/logrel/F_mu_ref_conc/examples/lock.v b/theories/logrel/F_mu_ref_conc/examples/lock.v
index 562d2d45..ba8a8a91 100644
--- a/theories/logrel/F_mu_ref_conc/examples/lock.v
+++ b/theories/logrel/F_mu_ref_conc/examples/lock.v
@@ -159,7 +159,7 @@ Section proof.
   Global Opaque with_lock.
 End proof.
 
-Global Hint Rewrite newlock_closed : autosubst.
-Global Hint Rewrite acquire_closed : autosubst.
-Global Hint Rewrite release_closed : autosubst.
-Global Hint Rewrite with_lock_subst : autosubst.
+Hint Rewrite newlock_closed : autosubst.
+Hint Rewrite acquire_closed : autosubst.
+Hint Rewrite release_closed : autosubst.
+Hint Rewrite with_lock_subst : autosubst.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
index 3309b710..d6a5b42b 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
@@ -79,7 +79,7 @@ Section CG_Stack.
   Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f].
   Proof. unfold CG_push; asimpl; trivial. Qed.
 
-  Global Hint Rewrite CG_push_subst : autosubst.
+  Hint Rewrite CG_push_subst : autosubst.
 
   Lemma steps_CG_push E ρ j K st v w :
     nclose specN ⊆ E →
@@ -451,13 +451,13 @@ Section CG_Stack.
 
 End CG_Stack.
 
-Global Hint Rewrite CG_push_subst : autosubst.
-Global Hint Rewrite CG_locked_push_subst : autosubst.
-Global Hint Rewrite CG_locked_pop_subst : autosubst.
-Global Hint Rewrite CG_pop_subst : autosubst.
-Global Hint Rewrite CG_locked_pop_subst : autosubst.
-Global Hint Rewrite CG_snap_subst : autosubst.
-Global Hint Rewrite CG_iter_subst : autosubst.
-Global Hint Rewrite CG_snap_iter_subst : autosubst.
-Global Hint Rewrite CG_stack_body_subst : autosubst.
-Global Hint Rewrite CG_stack_closed : autosubst.
+Hint Rewrite CG_push_subst : autosubst.
+Hint Rewrite CG_locked_push_subst : autosubst.
+Hint Rewrite CG_locked_pop_subst : autosubst.
+Hint Rewrite CG_pop_subst : autosubst.
+Hint Rewrite CG_locked_pop_subst : autosubst.
+Hint Rewrite CG_snap_subst : autosubst.
+Hint Rewrite CG_iter_subst : autosubst.
+Hint Rewrite CG_snap_iter_subst : autosubst.
+Hint Rewrite CG_stack_body_subst : autosubst.
+Hint Rewrite CG_stack_closed : autosubst.
diff --git a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
index 15e1073b..2b3d4661 100644
--- a/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
+++ b/theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
@@ -329,9 +329,9 @@ Section FG_stack.
 
 End FG_stack.
 
-Global Hint Rewrite FG_push_subst : autosubst.
-Global Hint Rewrite FG_pop_subst : autosubst.
-Global Hint Rewrite FG_iter_subst : autosubst.
-Global Hint Rewrite FG_read_iter_subst : autosubst.
-Global Hint Rewrite FG_stack_body_subst : autosubst.
-Global Hint Rewrite FG_stack_closed : autosubst.
+Hint Rewrite FG_push_subst : autosubst.
+Hint Rewrite FG_pop_subst : autosubst.
+Hint Rewrite FG_iter_subst : autosubst.
+Hint Rewrite FG_read_iter_subst : autosubst.
+Hint Rewrite FG_stack_body_subst : autosubst.
+Hint Rewrite FG_stack_closed : autosubst.
-- 
GitLab