From ec40350b68449943fe20c122c3d9e34c1c59d6f8 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Wed, 15 Feb 2017 14:55:47 +0100
Subject: [PATCH] Remove uses of iStartProof, which is intended as being an
internal tactic.
---
theories/typing/bool.v | 2 +-
theories/typing/int.v | 2 +-
theories/typing/type_context.v | 3 +--
3 files changed, 3 insertions(+), 4 deletions(-)
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 5806a9ee..a69d2e12 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -13,7 +13,7 @@ Section bool.
| [ #(LitInt (0|1))] => True
| _ => False
end%I |}.
- Next Obligation. intros ? [|[[| |[|[]|]]|] []]; iStartProof; auto. Qed.
+ Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto with I. Qed.
Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
Global Instance bool_send : Send bool.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index af9b3615..a7170246 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -12,7 +12,7 @@ Section int.
| [ #(LitInt z)] => True
| _ => False
end%I |}.
- Next Obligation. intros ? [|[[]|] []]; iStartProof; auto. Qed.
+ Next Obligation. intros ? [|[[]|] []]; auto with I. Qed.
Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
Global Instance int_send : Send int.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index dc0d11b9..c1eb0393 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -56,8 +56,7 @@ Section type_context.
destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
destruct v0; try discriminate; [].
destruct l; try discriminate; [].
- intros [=<-]. iStartProof. wp_bind p1.
- iApply (wp_wand with "[]").
+ intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
{ iApply IHp1. done. }
iIntros (v) "%". subst v. wp_op. done.
Qed.
--
GitLab