From f01228f27cff447c96525f01e511212ff44a12c4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 12:50:26 +0100
Subject: [PATCH] make solve_ne slightly more robust

---
 algebra/cofe.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index d75d8b187..ae0a93f7c 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;
-- 
GitLab