From 3967e7159c1e322e67eafb8f499db24a6841486d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Jan 2016 23:16:33 +0100
Subject: [PATCH] Variant of setoid_subst for individual variable.
---
modures/cofe.v | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/modures/cofe.v b/modures/cofe.v
index 1f249d37c..25eb6e1a9 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -7,7 +7,14 @@ 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 :=
+
+Tactic Notation "cofe_subst" ident(x) :=
+ repeat match goal with
+ | _ => progress simplify_equality'
+ | H:@dist ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist A d n) x
+ | H:@dist ?A ?d ?n _ x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
+ end.
+Tactic Notation "cofe_subst" :=
repeat match goal with
| _ => progress simplify_equality'
| H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x
--
GitLab