diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Cases.v | 9 | ||||
| -rw-r--r-- | test-suite/success/TestRefine.v | 9 |
2 files changed, 8 insertions, 10 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 499c066064..ccd92f6960 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -31,10 +31,11 @@ Type (* Interaction with coercions *) Parameter bool2nat : bool -> nat. Coercion bool2nat : bool >-> nat. -Check (fun x => match x with - | O => true - | S _ => 0 - end:nat). +Definition foo : nat -> nat := + fun x => match x with + | O => true + | S _ => 0 + end. (****************************************************************************) (* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 82c5cf2e74..dd84402dfa 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -9,13 +9,11 @@ (************************************************************************) Lemma essai : forall x : nat, x = x. - refine ((fun x0 : nat => match x0 with | O => _ | S p => _ - end) - :forall x : nat, x = x). (* x0=x0 et x0=x0 *) + end)). Restart. @@ -145,11 +143,10 @@ Lemma essai : forall n : nat, {x : nat | x = S n}. Restart. refine - ((fun n : nat => match n with + (fun n : nat => match n with | O => _ | S p => _ - end) - :forall n : nat, {x : nat | x = S n}). + end). Restart. |