From 8958d1a5bb66ba384c04b72f1c439187ddc428bc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 Jan 2016 06:59:52 +0100
Subject: [PATCH] Improve simplifier for option to handle unions.

---
 prelude/option.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/prelude/option.v b/prelude/option.v
index 865311fdc..bf66ba972 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -306,6 +306,10 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
   | _ => rewrite decide_False by tac
   | _ => rewrite option_guard_True by tac
   | _ => rewrite option_guard_False by tac
+  | H : context [None ∪ _] |- _ => rewrite (left_id_L None (∪)) in H
+  | H : context [_ ∪ None] |- _ => rewrite (right_id_L None (∪)) in H
+  | |- context [None ∪ _] => rewrite (left_id_L None (∪))
+  | |- context [_ ∪ None] => rewrite (right_id_L None (∪))
   end.
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
   repeat match goal with
-- 
GitLab