From ac07a76ee257c535b5686b49fd14c6d1e370cc9a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 12 Apr 2018 15:08:19 +0200
Subject: ssrnat: don't use `fix n` but rather `fix name n`

This was the proof does not depend on the lemma name.
---
 mathcomp/ssreflect/ssrnat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 0e5899a..4533103 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -726,7 +726,7 @@ have: forall n, P n -> n >= 0 by [].
 have: acc_nat 0.
   case exP => n; rewrite -(addn0 n); elim: n 0 => [|n IHn] j; first by left.
   by rewrite addSnnS; right; apply: IHn.
-move: 0; fix 2 => m IHm m_lb; case Pm: (P m); first by exists m.
+move: 0; fix find_ex_minn 2 => m IHm m_lb; case Pm: (P m); first by exists m.
 apply: find_ex_minn m.+1 _ _ => [|n Pn]; first by case: IHm; rewrite ?Pm.
 by rewrite ltn_neqAle m_lb //; case: eqP Pm => // -> /idP[].
 Qed.
-- 
cgit v1.2.3