fix more

Beluga-lang · May 15, 2024 · c7c6dca · c7c6dca
1 parent bdb61d4
commit c7c6dca
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v
@@ -332,7 +332,7 @@ Proof.
 Qed.
 
 
-#[global]
+#[export]
   Instance per_elem_PER {i R A B} `(H : per_univ_elem i R A B) : PER R.
 Proof.
   split.
@@ -341,7 +341,7 @@ Proof.
 Qed.
 
 
-#[global]
+#[export]
   Instance per_univ_PER {i R} : PER (per_univ_elem i R).
 Proof.
   split.
@@ -537,7 +537,7 @@ Proof.
 Qed.
 
 
-#[global]
+#[export]
   Instance per_ctx_PER {R} : PER (per_ctx_env R).
 Proof.
   split.
@@ -546,7 +546,7 @@ Proof.
 Qed.
 
 
-#[global]
+#[export]
   Instance per_env_PER {R Γ Δ} (H : per_ctx_env R Γ Δ) : PER R.
 Proof.
   split.