diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 6804c1720ada7d964251c4185682b2b26f4b684d..c0cf52f3635fa0fffd1afb1cd500221dad4685bb 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -179,7 +179,8 @@ Ltac f_contractive :=
   | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
   end;
   try match goal with
-  | |- dist_later ?n ?x ?y => destruct n as [|n]; [done|change (x ≡{n}≡ y)]
+  | |- @dist_later ?A ?n ?x ?y =>
+         destruct n as [|n]; [done|change (@dist A _ n x y)]
   end;
   try reflexivity.