From 01d12014855abe6adaea20bbb35b1e9beadff14e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Jan 2017 15:30:22 +0100
Subject: [PATCH] let solve_inG handle higher-arity functions for the \Sigma

---
 theories/base_logic/lib/own.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index f0a672be0..70130e826 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -21,8 +21,11 @@ Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 Ltac solve_inG :=
   (* Get all assumptions *)
   intros;
-  (* Unfold the top-level xΣ *)
+  (* Unfold the top-level xΣ. We need to support this to be a function. *)
   lazymatch goal with
+  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
+  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
   | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
   | H : subG ?xΣ _ |- _ => try unfold xΣ in H
   end;
-- 
GitLab