LG

Migration

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

Message d'erreur :

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

Avant :

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

Maintenant :

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

Message d'erreur :

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

Jusqu'à la version Coq 8.8 :

Implicit Arguments every_other_even [A].

A partir de la version Coq 8.9 :

Arguments every_other_even [A].

Jusqu'à la version Coq 8.11 :

SearchAbout leb.

Après la version Coq 8.11 :

Search leb.