diff --git a/modures/cofe.v b/modures/cofe.v
index 15b23fe8b8e872e182887faba6f8d3fceb62ebaa..2692e0b03214e7a8de526c7d8916b7bb84083f5e 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -11,8 +11,8 @@ 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
+  | 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.
 
 Record chain (A : Type) `{Dist A} := {