From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- test-suite/bugs/closed/4354.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/4354.v (limited to 'test-suite/bugs/closed/4354.v') diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v new file mode 100644 index 00000000..e71ddaf7 --- /dev/null +++ b/test-suite/bugs/closed/4354.v @@ -0,0 +1,11 @@ +Inductive True : Prop := I. +Class Lift (T : Type). +Axiom closed_increment : forall {T} {H : Lift T}, True. +Create HintDb core. +Lemma closed_monotonic T (H : Lift T) : True. +Proof. + Set Printing Universes. + auto using closed_increment. Show Universes. +Qed. +(* also fails with -nois, so the content of the hint database does not matter +*) \ No newline at end of file -- cgit v1.2.3