From a61c87a08258d540c809310976f494eafc4acea4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Jun 2014 18:14:11 +0200
Subject: [PATCH] Support structs/unions with named fields in frontend.

---
 theories/base.v   |  3 +++
 theories/option.v | 10 ++++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index a9c3cfdd..fd49fb6e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -419,6 +419,9 @@ Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
 Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+Notation "' ( x1 , x2 , x3  , x4 , x5 , x6 ) ← y ; z" :=
+  (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
+  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
diff --git a/theories/option.v b/theories/option.v
index 4df5d7e2..62641831 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -199,14 +199,16 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
   repeat match goal with
   | _ => progress simplify_equality'
   | _ => progress simpl_option_monad by tac
-  | H : mbind (M:=option) _ ?o = ?x |- _ =>
+  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    destruct o eqn:?
-  | H : ?x = mbind (M:=option) _ ?o |- _ =>
+    let y := fresh in destruct o as [y|] eqn:?;
+      [change (f y = x) in H|change (None = x) in H]
+  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    destruct o eqn:?
+    let y := fresh in destruct o as [y|] eqn:?;
+      [change (x = f y) in H|change (x = None) in H]
   | H : fmap (M:=option) _ ?o = ?x |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-- 
GitLab