From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- test-suite/bugs/closed/shouldsucceed/1302.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test-suite/bugs/closed/shouldsucceed/1302.v (limited to 'test-suite/bugs/closed/shouldsucceed/1302.v') diff --git a/test-suite/bugs/closed/shouldsucceed/1302.v b/test-suite/bugs/closed/shouldsucceed/1302.v new file mode 100644 index 00000000..e94dfcfb --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1302.v @@ -0,0 +1,22 @@ +Module Type T. + +Parameter A : Type. + +Inductive L : Type := +| L0 : L (* without this constructor, it works right *) +| L1 : A -> L. + +End T. + +Axiom Tp : Type. + +Module TT : T. + +Definition A : Type := Tp. + +Inductive L : Type := +| L0 : L +| L1 : A -> L. + +End TT. + -- cgit v1.2.3