diff options
| author | Enrico | 2018-04-12 17:14:20 +0200 |
|---|---|---|
| committer | GitHub | 2018-04-12 17:14:20 +0200 |
| commit | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (patch) | |
| tree | b95ac156d027c91f2103d33b46dbf5d2bcae33b8 /mathcomp | |
| parent | c17414bbef21bb3d0b96ee004c29ef7d56e55e2e (diff) | |
| parent | ac07a76ee257c535b5686b49fd14c6d1e370cc9a (diff) | |
Merge pull request #190 from gares/anon-fix
ssrnat: don't use `fix n` but rather `fix name n`
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |