diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index f67a22da5c0d6db82acce3404ed8a884ec77696e..9dfcbf9cdb31369556aeb987da4654ca2275a1b2 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,7 +1,5 @@
 Require Import Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language iris.parameter.
-
-Set Bullet Behavior "Strict Subproofs".
+Require Import prelude.option prelude.gmap iris.parameter.
 
 (** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
     They all assume such an equality is the first thing on the "stack" (goal). *)
diff --git a/iris/parameter.v b/iris/parameter.v
index 66a71493cf75d0d9aa6729a4c114c2578821f04f..cfbf73ee39c65de9138adace5faa06ee88e87e32 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -1,7 +1,5 @@
 Require Export modures.cmra iris.language.
 
-Set Bullet Behavior "Strict Subproofs".
-
 Record iParam := IParam {
   iexpr : Type;
   ival : Type;
@@ -29,6 +27,8 @@ Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
 Qed.
 
+Canonical Structure istateC Σ := leibnizC (istate Σ).
+
 Definition IParamConst {iexpr ival istate : Type}
            (ilanguage : Language iexpr ival istate)
            (icmra : cmraT) {icmra_empty : Empty icmra}
@@ -39,5 +39,3 @@ Unshelve.
 - by intros.
 - by intros.
 Defined.
-
-Canonical Structure istateC Σ := leibnizC (istate Σ).