From 5906df0662a103232fa49c55e1f87bafe2d2adb6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Jun 2019 20:23:28 +0200
Subject: [PATCH] Bump Iris (lazy_tc).
---
theories/logic/proofmode/tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 683799b..66a7b2f 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)
--
GitLab