diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 683799bf5b9494f866abe0939ed32371351f6782..66a7b2f807bb2f8f33a355a0cbc7e107e397a778 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -93,7 +93,7 @@ Ltac rel_values :=
   rel_finish.
 
 Tactic Notation "rel_apply_l" open_constr(lem) :=
-  (iPoseProofCore lem as false true (fun H =>
+  (iPoseProofCore lem as false (fun H =>
     rel_reshape_cont_l ltac:(fun K e =>
       rel_bind_ctx_l K;
       iApplyHyp H)
@@ -108,7 +108,7 @@ Tactic Notation "rel_apply_l" open_constr(lem) :=
   try rel_finish.
 
 Tactic Notation "rel_apply_r" open_constr(lem) :=
-  (iPoseProofCore lem as false true (fun H =>
+  (iPoseProofCore lem as false (fun H =>
     rel_reshape_cont_r ltac:(fun K e =>
       rel_bind_ctx_r K;
       iApplyHyp H)