From 8c382d564ca65b6e88e226e28de49a81d895fe64 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 5 Jan 2016 22:25:28 +0100
Subject: [PATCH] make proof of fill_not_value fully automatic

---
 channel/heap_lang.v | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/channel/heap_lang.v b/channel/heap_lang.v
index d3bd55592..9d8ecbb6c 100644
--- a/channel/heap_lang.v
+++ b/channel/heap_lang.v
@@ -181,12 +181,7 @@ Qed.
 Lemma fill_not_value e K :
   e2v e = None -> e2v (fill K e) = None.
 Proof.
-  intros Hnval.  induction K =>/=; try reflexivity.
-  - done.
-  - by rewrite IHK /=.
-  - by rewrite v2v /= IHK /=.
-  - by rewrite IHK /=.
-  - by rewrite IHK /=.
+  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
 Qed.
 
 Lemma fill_not_value2 e K v :
-- 
GitLab