diff --git a/prelude/collections.v b/prelude/collections.v
index 1f7c67af6a199a63ffd0daa805e2c14f86e0d02b..dedf2d24fbcb5f74b9d945edda3dd6678c037838 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -140,7 +140,7 @@ Hint Mode SetUnfold + - : typeclass_instances.
 Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
 Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
 
-Instance set_unfold_fallthrough P : SetUnfold P P | 1000. done. Qed.
+Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
 Definition set_unfold_1 `{SetUnfold P Q} : P → Q := proj1 (set_unfold P Q).
 Definition set_unfold_2 `{SetUnfold P Q} : Q → P := proj2 (set_unfold P Q).
 
diff --git a/proofmode/classes.v b/proofmode/classes.v
index b8d444380cc0e820727c3090cb7c5344bf3c6388..d2e0eefd3ad2fec06d6fb4b1fd6ab04b3c7c16b6 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -52,7 +52,7 @@ Global Arguments into_later _ _ {_}.
 Class FromLater (P Q : uPred M) := from_later : ▷ Q ⊢ P.
 Global Arguments from_later _ _ {_}.
 
-Global Instance into_later_fallthrough P : IntoLater P P | 1000.
+Global Instance into_later_default P : IntoLater P P | 1000.
 Proof. apply later_intro. Qed.
 Global Instance into_later_later P : IntoLater (â–· P) P.
 Proof. done. Qed.
@@ -222,7 +222,7 @@ Global Instance make_sep_true_l P : MakeSep True P P.
 Proof. by rewrite /MakeSep left_id. Qed.
 Global Instance make_sep_true_r P : MakeSep P True P.
 Proof. by rewrite /MakeSep right_id. Qed.
-Global Instance make_sep_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
+Global Instance make_sep_default P Q : MakeSep P Q (P ★ Q) | 100.
 Proof. done. Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9.
@@ -236,7 +236,7 @@ Global Instance make_and_true_l P : MakeAnd True P P.
 Proof. by rewrite /MakeAnd left_id. Qed.
 Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
-Global Instance make_and_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
+Global Instance make_and_default P Q : MakeSep P Q (P ★ Q) | 100.
 Proof. done. Qed.
 Global Instance frame_and_l R P1 P2 Q Q' :
   Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
@@ -250,7 +250,7 @@ Global Instance make_or_true_l P : MakeOr True P True.
 Proof. by rewrite /MakeOr left_absorb. Qed.
 Global Instance make_or_true_r P : MakeOr P True True.
 Proof. by rewrite /MakeOr right_absorb. Qed.
-Global Instance make_or_fallthrough P Q : MakeOr P Q (P ∨ Q) | 100.
+Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. done. Qed.
 Global Instance frame_or R P1 P2 Q1 Q2 Q :
   Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
@@ -259,7 +259,7 @@ Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
 Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
 Global Instance make_later_true : MakeLater True True.
 Proof. by rewrite /MakeLater later_True. Qed.
-Global Instance make_later_fallthrough P : MakeLater P (â–· P) | 100.
+Global Instance make_later_default P : MakeLater P (â–· P) | 100.
 Proof. done. Qed.
 
 Global Instance frame_later R P Q Q' :
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index e35620930014910c450599f4688884f1663317ff..311a4d0ce2b143ed8934463438206045f17d5245 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -453,7 +453,7 @@ Qed.
 Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
   into_assert : R ★ (P -★ Q) ⊢ Q.
 Global Arguments into_assert _ _ _ {_}.
-Lemma into_assert_fallthrough P Q : IntoAssert P Q P.
+Lemma into_assert_default P Q : IntoAssert P Q P.
 Proof. by rewrite /IntoAssert wand_elim_r. Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 63e04aed97486700d750fa3dc2233740f2d4083e..7e21c1739a94cf4e53ff18cf525f353b92be2d89 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -194,7 +194,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |match k with
-          | GoalStd => apply into_assert_fallthrough
+          | GoalStd => apply into_assert_default
           | GoalPvs => apply _ || fail "iSpecialize: cannot generate pvs goal"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
@@ -752,7 +752,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
   | [SGoal ?k ?lr ?Hs] =>
      eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
        [match k with
-        | GoalStd => apply into_assert_fallthrough
+        | GoalStd => apply into_assert_default
         | GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
         end
        |env_cbv; reflexivity || fail "iAssert:" Hs "not found"