From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/5300.v | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 test-suite/bugs/closed/5300.v (limited to 'test-suite/bugs/closed/5300.v') diff --git a/test-suite/bugs/closed/5300.v b/test-suite/bugs/closed/5300.v new file mode 100644 index 00000000..18202df5 --- /dev/null +++ b/test-suite/bugs/closed/5300.v @@ -0,0 +1,39 @@ +Module Test1. + + Module Type Foo. + Parameter t : unit. + End Foo. + + Module Bar : Foo. + Module Type Rnd. Definition t' : unit := tt. End Rnd. + Module Rnd_inst : Rnd. Definition t' : unit := tt. End Rnd_inst. + Definition t : unit. + exact Rnd_inst.t'. + Qed. + End Bar. + + Print Assumptions Bar.t. +End Test1. + +Module Test2. + Module Type Foo. + Parameter t1 : unit. + Parameter t2 : unit. + End Foo. + + Module Bar : Foo. + Inductive ind := . + Definition t' : unit := tt. + Definition t1 : unit. + Proof. + exact ((fun (_ : ind -> False) => tt) (fun H => match H with end)). + Qed. + Definition t2 : unit. + Proof. + exact t'. + Qed. + End Bar. + + Print Assumptions Bar.t1. + Print Assumptions Bar.t1. +End Test2. -- cgit v1.2.3