From 6f504682be5cef85a4803e1796fbdb92a645f0a8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 8 Feb 2015 18:17:49 +0100
Subject: [PATCH] Improve case_option_guard to destruct on decide P in case of
 mguard P.

First it would destruct on the decider, which sometimes would result
in unfolded hypotheses.
---
 theories/option.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/option.v b/theories/option.v
index edb10293..2878f33b 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -204,12 +204,14 @@ End option_union_intersection_difference.
 (** * Tactics *)
 Tactic Notation "case_option_guard" "as" ident(Hx) :=
   match goal with
-  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
-    let X := context C [ match dec with left H => x H | _ => None end ] in
-    change X in H; destruct_decide dec as Hx
-  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
-    let X := context C [ match dec with left H => x H | _ => None end ] in
-    change X; destruct_decide dec as Hx
+  | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
+    change (@mguard option _ P dec) with (λ A (x : P → option A),
+      match @decide P dec with left H' => x H' | _ => None end) in *;
+    destruct_decide (@decide P dec) as Hx
+  | |- appcontext C [@mguard option _ ?P ?dec] =>
+    change (@mguard option _ P dec) with (λ A (x : P → option A),
+      match @decide P dec with left H' => x H' | _ => None end) in *;
+    destruct_decide (@decide P dec) as Hx
   end.
 Tactic Notation "case_option_guard" :=
   let H := fresh in case_option_guard as H.
-- 
GitLab