From c5bdf6220614f85859f06a51d177ffb8d67e4053 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Jun 2015 20:13:04 +0200
Subject: [PATCH] Make function environments a parameter of assertions.

---
 theories/base.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index cc1938b0..82c6b8d6 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -165,6 +165,11 @@ Instance: Params (@equivE) 4.
 Notation "X ≡{ Γ } Y" := (equivE Γ X Y)
   (at level 70, format "X  ≡{ Γ }  Y") : C_scope.
 Notation "(≡{ Γ } )" := (equivE Γ) (only parsing, Γ at level 1) : C_scope.
+Notation "X ≡{ Γ1 , Γ2 , .. , Γ3 } Y" :=
+  (equivE (pair .. (Γ1, Γ2) .. Γ3) X Y)
+  (at level 70, format "'[' X  ≡{ Γ1 , Γ2 , .. , Γ3 }  '/' Y ']'") : C_scope.
+Notation "(≡{ Γ1 , Γ2 , .. , Γ3 } )" := (equivE (pair .. (Γ1, Γ2) .. Γ3))
+  (only parsing, Γ1 at level 1) : C_scope.
 
 (** The type class [LeibnizEquiv] collects setoid equalities that coincide
 with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
-- 
GitLab