From d7f8ff30c9285e4a2a60a4512104a5570a9e5084 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Nov 2017 22:34:38 +0100
Subject: [PATCH] Turn the proof mode's `option_bind` into a definition.

It used to be an inline pattern match.

This also restores compatibility with Coq 8.6.1.
---
 theories/proofmode/base.v         | 4 ++++
 theories/proofmode/coq_tactics.v  | 2 +-
 theories/proofmode/environments.v | 6 ++++--
 theories/proofmode/tactics.v      | 1 +
 4 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 4ff779335..9497be345 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -83,3 +83,7 @@ Qed.
 
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
+
+Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
+  match mx with Some x => f x | None => None end.
+Arguments option_bind _ _ _ !_ /.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index dafac376d..a6729546d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -361,7 +361,7 @@ Proof.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
-  destruct d; simplify_eq; solve_sep_entails.
+  destruct d; simplify_eq/=; solve_sep_entails.
 Qed.
 
 Global Instance envs_Forall2_refl (R : relation (uPred M)) :
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index c3136b8b8..d980e776f 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -17,8 +17,8 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   end.
 
 Module env_notations.
-  Notation "y ≫= f" := (match y with Some x => f x | None => None end).
-  Notation "x ← y ; z" := (match y with Some x => z | None => None end).
+  Notation "y ≫= f" := (option_bind f y).
+  Notation "x ← y ; z" := (y ≫= λ x, z).
   Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
   Notation "Γ !! j" := (env_lookup j Γ).
 End env_notations.
@@ -93,6 +93,8 @@ Ltac simplify :=
   | _ => progress simplify_eq/=
   | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
   | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
+  | H : context [option_bind _ ?x] |- _ => destruct x eqn:?
+  | |- context [option_bind _ ?x] => destruct x eqn:?
   | _ => case_match
   end.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 94c2de629..36b2006c6 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -8,6 +8,7 @@ Set Default Proof Using "Type".
 Export ident.
 
 Declare Reduction env_cbv := cbv [
+  option_bind
   beq ascii_beq string_beq positive_beq ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_persistent env_spatial env_spatial_is_nil envs_dom
-- 
GitLab