summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1618.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1618.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1618.v23
1 files changed, 0 insertions, 23 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v
deleted file mode 100644
index a9b067ce..00000000
--- a/test-suite/bugs/closed/shouldsucceed/1618.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Inductive A: Set :=
-| A1: nat -> A.
-
-Definition A_size (a: A) : nat :=
- match a with
- | A1 n => 0
- end.
-
-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
- | A1 n => f n
- end.
-
-
-Function n1 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {measure A_size a} :
-P
-a :=
- match a return (P a) with
- | A1 n => f n
- end.
-