add some missing visibility hints

theories/lang/lang.v

@@ -3,7 +3,7 @@ From stdpp Require Export strings binders.
 From stdpp Require Import gmap.
 From iris.prelude Require Import options.
 
-Open Scope Z_scope.
+Global Open Scope Z_scope.
 
 (** Expressions and vals. *)
 Definition block : Set := positive.
@@ -12,7 +12,7 @@ Definition loc : Set := block * Z.
 Declare Scope loc_scope.
 Bind Scope loc_scope with loc.
 Delimit Scope loc_scope with L.
-Open Scope loc_scope.
+Global Open Scope loc_scope.
 
 Inductive base_lit : Set :=
 | LitPoison | LitLoc (l : loc) | LitInt (n : Z).
@@ -43,8 +43,8 @@ Inductive expr :=
 | Case (e : expr) (el : list expr)
 | Fork (e : expr).
 
-Arguments App _%E _%E.
-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.
-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.
-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.

theories/lang/tactics.v

@@ -229,8 +229,8 @@ Ltac simpl_subst :=
       rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
   end;
   unfold W.to_expr; simpl.
-Arguments W.to_expr : simpl never.
-Arguments subst : simpl never.
+Global Arguments W.to_expr : simpl never.
+Global Arguments subst : simpl never.
 
 (** The tactic [inv_head_step] performs inversion on hypotheses of the
 shape [head_step]. The tactic will discharge head-reductions starting

theories/lifetime/model/definitions.v

@@ -17,7 +17,7 @@ Module Export lft_notation.
 End lft_notation.
 
 Definition static : lft := (∅ : gmultiset _).
-Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
+Global Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
 Definition positive_to_lft (p : positive) : lft := {[+ p +]}.
 

theories/typing/base.v

@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
    sets coming from the prelude. *)
 From lrust.lang.lib Require Export new_delete.
 
-Open Scope Z_scope.
+Global Open Scope Z_scope.
 
 Definition lft_userN : namespace := nroot .@ "lft_usr".
 

theories/typing/type.v

@@ -45,10 +45,10 @@ Record type `{!typeGS Σ} :=
     ty_shr_mono κ κ' tid l :
       κ' ⊑ κ -∗ ty_shr κ tid l -∗ ty_shr κ' tid l
   }.
-Existing Instance ty_shr_persistent.
-Instance: Params (@ty_size) 2 := {}.
-Instance: Params (@ty_own) 2 := {}.
-Instance: Params (@ty_shr) 2 := {}.
+Global Existing Instance ty_shr_persistent.
+Global Instance: Params (@ty_size) 2 := {}.
+Global Instance: Params (@ty_own) 2 := {}.
+Global Instance: Params (@ty_shr) 2 := {}.
 
 Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
@@ -116,7 +116,7 @@ Record simple_type `{!typeGS Σ} :=
   { st_own : thread_id → list val → iProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
-Existing Instance st_own_persistent.
+Global Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2 := {}.
 
 Program Definition ty_of_st `{!typeGS Σ} (st : simple_type) : type :=
@@ -283,7 +283,7 @@ Section type_dist2.
 
   Definition type_dist2_later (n : nat) ty1 ty2 : Prop :=
     match n with O => True | S n => type_dist2 n ty1 ty2 end.
-  Arguments type_dist2_later !_ _ _ /.
+  Global Arguments type_dist2_later !_ _ _ /.
 
   Global Instance type_dist2_later_equivalence n :
     Equivalence (type_dist2_later n).