diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1618.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1618.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v index a90290bf..a9b067ce 100644 --- a/test-suite/bugs/closed/shouldsucceed/1618.v +++ b/test-suite/bugs/closed/shouldsucceed/1618.v @@ -6,7 +6,7 @@ Definition A_size (a: A) : nat := | A1 n => 0 end. -Require Import Recdef. +Require Import Recdef. Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a := match a return (P a) with |