From c55ce76d477f0f84f928d3efe03fcb7ca8584525 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Nov 2015 13:40:53 +0100
Subject: [PATCH] Subst tactic for the distance relation of a metric.

---
 iris/cofe.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/iris/cofe.v b/iris/cofe.v
index 7e667277c..f0cd655a8 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -8,6 +8,12 @@ Notation "x ={ n }= y" := (dist n x y)
   (at level 70, n at next level, format "x  ={ n }=  y").
 Hint Extern 0 (?x ={_}= ?x) => reflexivity.
 Hint Extern 0 (_ ={_}= _) => symmetry; assumption.
+Ltac cofe_subst :=
+  repeat match goal with
+  | _ => progress simplify_equality'
+  | H: @dist _ ?d ?n ?x _ |- _ => setoid_subst_aux (@dist _ d n) x
+  | H: @dist _ ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist _ d n) x
+  end.
 
 Record chain (A : Type) `{Dist A} := {
   chain_car :> nat → A;
-- 
GitLab