diff options
Diffstat (limited to 'test-suite/success/Funind.v')
| -rw-r--r-- | test-suite/success/Funind.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 3bf97c13..f87f2e2a 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -1,4 +1,6 @@ +Require Import Coq.funind.FunInd. + Definition iszero (n : nat) : bool := match n with | O => true |