=====Migration=====

====Fonctions====

===NArith, PArith, ZArith===

Voir commit [[https://github.com/rocq-prover/rocq/commit/b1162463d577baf450c3f33ab880e7d9afe21148|''b1162463d577baf450c3f33ab880e7d9afe21148''. Les fonctions commençant par ''N'', ''P'' ou ''Z'' ont été déplacées dans leur propre ''namespace''.

Jusqu'à la version Coq 8.9 :

  Ncompare

A partir de la version Coq 8.10 :

  N.compare

===_ doit être mis après match ... with===

Message d'erreur :

  The constructor XXX (in type yyy) expects 1 argument.

Avant :

<code>
Compute match N' nat 2 (L' nat) (N' nat 3 (L' nat) (L' nat)) with
    L' => L' nat
  | N' x t t' => t'
  end.
</code>

Maintenant :

<code>
Compute match N' nat 2 (L' nat) (N' nat 3 (L' nat) (L' nat)) with
    L' _ => L' nat
  | N' _ x t t' => t'
  end.
</code>

===Implicit Arguments===

Message d'erreur :

  Syntax error: 'Type' or 'Types' expected after 'Implicit' (in [vernac:gallina_ext]).

Jusqu'à la version Coq 8.8 :

<code>
Implicit Arguments every_other_even [A].
</code>

A partir de la version Coq 8.9 :

<code>
Arguments every_other_even [A].
</code>

===SearchAbout===

Jusqu'à la version Coq 8.11 :

<code>
SearchAbout leb.
</code>

Après la version Coq 8.11 :

<code>
Search leb.
</code>

=====Exemples=====

Coq'Art : {{ :lang:rocq:mise_a_jour:coq-art-8.1.tar.gz |8.1}}, {{ :lang:rocq:mise_a_jour:coq-art-8.2.tar.gz |8.2}}, {{ :lang:rocq:mise_a_jour:coq-art-8.3.tar.gz |8.3}}, {{ :lang:rocq:mise_a_jour:coq-art-8.4.tar.gz |8.4}}, {{ :lang:rocq:mise_a_jour:coq-art-8.5.tar.gz |8.5}}, {{ :lang:rocq:mise_a_jour:coq-art-8.6.tar.gz |8.6}}, {{ :lang:rocq:mise_a_jour:coq-art-8.7.tar.gz |8.7}}, {{ :lang:rocq:mise_a_jour:coq-art-8.9.0.tar.gz |8.9}}, {{ :lang:rocq:mise_a_jour:coq-art-8.10.0.tar.gz |8.10}}, {{ :lang:rocq:mise_a_jour:coq-art-8.11.0.tar.gz |8.11}}, {{ :lang:rocq:mise_a_jour:coq-art-8.12.0.tar.gz |8.12}}, {{ :lang:rocq:mise_a_jour:coq-art-8.13.0.tar.gz |8.13}}, {{ :lang:rocq:mise_a_jour:coq-art-8.14.0.tar.gz |8.14}}, {{ :lang:rocq:mise_a_jour:coq-art-8.15.0.tar.gz |8.15}}, {{ :lang:rocq:mise_a_jour:coq-art-8.20.0.tar.gz |8.20}},