diff options
| -rw-r--r-- | test-suite/success/Cases.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index e9af06f39a..e2e9454e25 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -2274,3 +2274,7 @@ end. (* ------------------------------------------------------------------ *) End Sig. + +(* Test de la syntaxe avec nombres *) +Require Arith. +Check [n] Cases n of 2 => true | _ => false end.
\ No newline at end of file |