From 3ac5cc065138fa6293ed348668b08c13f36d221a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 Feb 2015 01:47:33 +0100
Subject: [PATCH] Add shallow embedded assertion language.

Ported from popl2014 branch.
---
 theories/base.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index e753fb73..409bc389 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -160,6 +160,12 @@ Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : C_scope.
 Notation "( X ≢)" := (λ Y, X ≢ Y) (only parsing) : C_scope.
 Notation "(≢ X )" := (λ Y, Y ≢ X) (only parsing) : C_scope.
 
+Class EquivE E A := equivE: E → relation A.
+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.
+
 (** The type class [LeibnizEquiv] collects setoid equalities that coincide
 with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
@@ -192,6 +198,8 @@ equality. *)
 Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
 Hint Extern 0 (_ ≡ _) => reflexivity.
 Hint Extern 0 (_ ≡ _) => symmetry; assumption.
+Hint Extern 0 (_ ≡{_} _) => reflexivity.
+Hint Extern 0 (_ ≡{_} _) => symmetry; assumption.
 
 (** ** Operations on collections *)
 (** We define operational type classes for the traditional operations and
-- 
GitLab