From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/bugs/closed/4450.v | 58 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 test-suite/bugs/closed/4450.v

(limited to 'test-suite/bugs/closed/4450.v')

diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v
new file mode 100644
index 00000000..ecebaba8
--- /dev/null
+++ b/test-suite/bugs/closed/4450.v
@@ -0,0 +1,58 @@
+Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop.
+
+Polymorphic Axiom unit@{u} : Type@{u}.
+Polymorphic Axiom tt@{u} : inhabited unit@{u}.
+
+Polymorphic Hint Resolve tt : the_lemmas.
+Set Printing All.
+Set Printing Universes.
+Goal inhabited unit.
+Proof.
+  eauto with the_lemmas.
+Qed.
+
+Universe u.
+Axiom f : Type@{u} -> Prop.
+Lemma fapp (X : Type) : f X -> False.
+Admitted.
+Polymorphic Axiom funi@{i} : f unit@{i}.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto using (fapp unit funi). (* The two fapp's have different universes *)
+Qed.
+
+Hint Resolve (fapp unit funi) : mylems.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto with mylems. (* Forces the two fapps at the same level *)
+Qed.
+
+Goal (forall U, f U) -> (f unit -> False) -> False /\ False.
+  eauto. (* Forces the two fapps at the same level *)
+Qed.
+
+Polymorphic Definition MyType@{i} := Type@{i}.
+Universes l m n.
+Constraint l < m.
+Polymorphic Axiom maketype@{i} : MyType@{i}.
+
+Goal MyType@{l}.
+Proof.
+  Fail solve [ eauto using maketype@{m} ].
+  eauto using maketype.
+  Undo.
+  eauto using maketype@{n}.
+Qed.
+
+Axiom foo : forall (A : Type), list A.
+Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A.
+
+Universe x y.
+Goal list Type@{x}.
+Proof.
+  eauto using (foo Type). (* Refreshes the term *)
+  Undo.
+  eauto using foo. Show Universes.
+  Undo.
+  eauto using foop. Show Proof. Show Universes.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3