aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4354.v
blob: e71ddaf71f0e263409cd261a03999d96d93b08db (plain)
1
2
3
4
5
6
7
8
9
10
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
*)