fix argument scope warnings

lambda-rust/lang/lang.v

@@ -43,8 +43,8 @@ Inductive expr :=
 | Case (e : expr) (el : list expr)
 | Fork (e : expr).
 
-Global Arguments App _%E _%E.
-Global Arguments Case _%E _%E.
+Global Arguments App _%_E _%_E.
+Global Arguments Case _%_E _%_E.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
@@ -151,12 +151,12 @@ Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :
   | x::xl, es::esl => subst' x es <$> subst_l xl esl e
   | _, _ => None
   end.
-Global Arguments subst_l _%binder _ _%E.
+Global Arguments subst_l _%_binder _ _%_E.
 
 Definition subst_v (xl : list binder) (vsl : vec val (length xl))
                    (e : expr) : expr :=
   Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
-Global Arguments subst_v _%binder _ _%E.
+Global Arguments subst_v _%_binder _ _%_E.
 
 Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
   Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.

lambda-rust/typing/programs.v

@@ -12,7 +12,7 @@ Section typing.
     (∀ tid (qmax : Qp), lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp qmax L -∗
                cctx_interp tid qmax C -∗ tctx_interp tid T -∗
                WP e {{ _, cont_postcondition }})%I.
-  Global Arguments typed_body _ _ _ _ _%E.
+  Global Arguments typed_body _ _ _ _ _%_E.
 
   Global Instance typed_body_llctx_permut E :
     Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
@@ -61,7 +61,7 @@ Section typing.
               llctx_interp qmax L -∗ tctx_interp tid T1 -∗
               WP e {{ v, na_own tid ⊤ ∗
                          llctx_interp qmax L ∗ tctx_interp tid (T2 v) }})%I.
-  Global Arguments typed_instruction _ _ _ _%E _.
+  Global Arguments typed_instruction _ _ _ _%_E _.
 
   (** Writing and Reading **)
   Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
@@ -73,7 +73,7 @@ Section typing.
   Definition typed_write_aux : seal (@typed_write_def). Proof. by eexists. Qed.
   Definition typed_write := typed_write_aux.(unseal).
   Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
-  Global Arguments typed_write _ _ _%T _%T _%T.
+  Global Arguments typed_write _ _ _%_T _%_T _%_T.
 
   Global Instance typed_write_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
     Persistent (typed_write E L ty1 ty ty2).
@@ -94,7 +94,7 @@ Section typing.
   Definition typed_read_aux : seal (@typed_read_def). Proof. by eexists. Qed.
   Definition typed_read := typed_read_aux.(unseal).
   Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
-  Global Arguments typed_read _ _ _%T _%T _%T.
+  Global Arguments typed_read _ _ _%_T _%_T _%_T.
 
   Global Instance typed_read_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
     Persistent (typed_read E L ty1 ty ty2).
@@ -104,11 +104,11 @@ End typing.
 Definition typed_instruction_ty `{!typeGS Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : iProp Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
-Global Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
+Global Arguments typed_instruction_ty {_ _} _ _ _ _%_E _%_T.
 
 Definition typed_val `{!typeGS Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
-Global Arguments typed_val _ _ _%V _%T.
+Global Arguments typed_val _ _ _%_V _%_T.
 
 Section typing_rules.
   Context `{!typeGS Σ}.