LG

Voir commit b1162463d577baf450c3f33ab880e7d9afe21148. Les fonctions commençant par N, P ou 'Z ont été déplacées dans leur propre namespace''.

Avant :

Ncompare

Après :

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]).

Avant :

Implicit Arguments every_other_even [A].

Après :

Arguments every_other_even [A].