From 79ea27b35e8f8ead0facdafbd00cb81a3c0f6dde Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Jul 2018 09:37:10 +0200
Subject: [PATCH] proofmode: normalize big_opL

---
 tests/proofmode.v              | 2 +-
 theories/proofmode/reduction.v | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index d2ba302b5..f558964ab 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -490,7 +490,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
   ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
   P.
-Proof. iIntros "HP ?? /=". Show. done. Qed.
+Proof. iIntros "HP ??". Show. done. Qed.
 
 Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P -∗
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 0d05f3794..3dd260e5a 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -22,7 +22,8 @@ Declare Reduction pm_cbn := cbn [
   tele_fold tele_bind tele_app
   (* BI connectives *)
   bi_persistently_if bi_affinely_if bi_intuitionistically_if
-  bi_wandM bi_tforall bi_texist
+  bi_wandM big_opL
+  bi_tforall bi_texist
 ].
 Ltac pm_eval t :=
   let u := eval pm_cbv in t in
-- 
GitLab