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 :

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.