From de9438cb45f8052fe863b5e10417fe154cca4c15 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jul 2016 17:02:20 +0200
Subject: [PATCH] Declare inG arguments of own_* implicit but not maximally
 inserted.

This way type class inference is not invokved when used in tactics
like iPvs while not having to write an @.

(Idea suggested by Ralf.)
---
 heap_lang/lib/spawn.v           | 2 +-
 program_logic/auth.v            | 4 ++--
 program_logic/boxes.v           | 2 +-
 program_logic/ghost_ownership.v | 6 ++++++
 program_logic/sts.v             | 4 ++--
 tests/joining_existentials.v    | 2 +-
 tests/one_shot.v                | 6 +++---
 7 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 221ca9b80..4c2617a7f 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -80,7 +80,7 @@ Proof.
     + iPvsIntro; iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame; eauto. }
       wp_match. by iApply "Hv".
-    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (@own_valid with "Hγ") as %[].
+    + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
 Qed.
 End proof.
 
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 2c1694508..ba098d733 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -103,14 +103,14 @@ Section auth.
     iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
     iInv N as (a') "[Hγ Hφ]".
     iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
-    iDestruct (@own_valid with "#Hγ") as "Hvalid".
+    iDestruct (own_valid with "#Hγ") as "Hvalid".
     iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
     iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
     rewrite ->(left_id _ _) in Ha'; setoid_subst.
     iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
     { iApply "HΨ"; by iSplit. }
     iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
-    iPvs (@own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
+    iPvs (own_update with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
     iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
     iNext. iExists (b â‹… af). by iFrame.
   Qed.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index e81180b79..793b69c51 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -69,7 +69,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 :
 Proof.
   rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".
   iDestruct "Hb" as % [[[] [= ->]%leibniz_equiv] ?]%auth_valid_discrete.
-  iApply (@own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
+  iApply (own_update with "Hγ"); apply prod_update; simpl; last reflexivity.
   by apply auth_update_no_frame, option_local_update, exclusive_local_update.
 Qed.
 
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index cd679ccdf..92c4adc27 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -82,6 +82,12 @@ Proof.
 Qed.
 End global.
 
+Arguments own_valid {_ _ _} [_] _ _.
+Arguments own_valid_l {_ _ _} [_] _ _.
+Arguments own_valid_r {_ _ _} [_] _ _.
+Arguments own_updateP {_ _ _} [_] _ _ _ _ _.
+Arguments own_update {_ _ _} [_] _ _ _ _ _.
+
 Section global_empty.
 Context `{i : inG Λ Σ (A:ucmraT)}.
 Implicit Types a : A.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 7152d178f..a8180d0e9 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -102,14 +102,14 @@ Section sts.
   Proof.
     iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
     iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ".
-    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (@own_valid with "#Hγ") as %Hvalid.
+    iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
     assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
     iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
     iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
     { iApply "HΨ"; by iSplit. }
     iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)".
-    iPvs (@own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
+    iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
     iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
     iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
     iNext; iExists s'; by iFrame.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 36077d52e..97f37f828 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -84,7 +84,7 @@ Proof.
   iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
   - wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
-    iPvs (@own_update with "Hγ") as "Hx".
+    iPvs (own_update with "Hγ") as "Hx".
     { by apply (cmra_update_exclusive (Shot x)). }
     iApply signal_spec; iFrame "Hs"; iSplit; last done.
     iExists x; auto.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index faaac9314..66479873d 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -51,7 +51,7 @@ Proof.
   - iIntros (n) "!". wp_let.
     iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
     + wp_cas_suc. iSplitL; [|by iLeft].
-      iPvs (@own_update with "Hγ") as "Hγ".
+      iPvs (own_update with "Hγ") as "Hγ".
       { by apply cmra_update_exclusive with (y:=Shot n). }
       iPvsIntro; iRight; iExists n; by iSplitL "Hl".
     + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
@@ -72,10 +72,10 @@ Proof.
     { by wp_match. }
     wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]".
-    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (@own_valid with "Hγ") as %?. }
+    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
     wp_load; iPvsIntro.
     iCombine "Hγ" "Hγ'" as "Hγ".
-    iDestruct (@own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
+    iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
     wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
 Qed.
-- 
GitLab