From 0429c257e3088cf77c8852a2cbeff2b02671b8b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Mar 2017 15:10:04 +0200
Subject: [PATCH] Consider simpl and clearing introduction patterns as
persistent.
This fixes the bug that when having:
iDestruct (foo with "H") as "{H1 H2} #[H1 H2]"
The hypothesis H would not be kept.
---
theories/proofmode/intro_patterns.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 2a6cac321..39a28f98b 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -144,6 +144,9 @@ Fixpoint intro_pat_persistent (p : intro_pat) :=
| IPureElim => true
| IAlwaysElim _ => true
| IList pps => forallb (forallb intro_pat_persistent) pps
+ | ISimpl => true
+ | IClear _ => true
+ | IClearFrame _ => true
| _ => false
end.
--
GitLab