diff --git a/modures/cofe.v b/modures/cofe.v
index 1f249d37c99c05f3947983b4b2195e8f16d08645..25eb6e1a9cf4904d22b635cb18b026d680e84ca9 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