diff --git a/algebra/cofe.v b/algebra/cofe.v
index d75d8b18712d342c99fac57fe44ebb33c6b9cb9b..ae0a93f7cb43bd2d121ccfe32b70af1036c269e3 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -21,7 +21,7 @@ Tactic Notation "cofe_subst" :=
   | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
   end.
 
-Tactic Notation "solve_ne" := move=>n; solve_proper.
+Tactic Notation "solve_ne" := intros; solve_proper.
 
 Record chain (A : Type) `{Dist A} := {
   chain_car :> nat → A;