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

@@ -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 _ _ _ !_ /.

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)) :

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.
 

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