From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/1618.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test-suite/bugs/closed/1618.v (limited to 'test-suite/bugs/closed/1618.v') diff --git a/test-suite/bugs/closed/1618.v b/test-suite/bugs/closed/1618.v new file mode 100644 index 00000000..a9b067ce --- /dev/null +++ b/test-suite/bugs/closed/1618.v @@ -0,0 +1,23 @@ +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. + -- cgit v1.2.3