Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers

2 files changed, 25 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index cd9cad4064..7bed956f3e 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) :=
     morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d)
   }.
 
+(** Workaround to simpl losing universe constraints, see bug #5645. *)
+Ltac simpl' :=
+  simpl; match goal with [ |- ?P ] => let T := type of P in idtac end.
+
 Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
 : IsTrunc n (forall a, P a) | 100.
 Proof.
     generalize dependent P.
-  induction n as [ | n' IH]; (simpl; intros P ?).
+  induction n as [ | n' IH]; (simpl'; intros P ?).
   - admit.
   - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit.
 Defined.
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
new file mode 100644
index 0000000000..b736b734fd
--- /dev/null
+++ b/test-suite/success/abstract_poly.v
@@ -0,0 +1,20 @@
+Set Universe Polymorphism.
+
+Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x.
+Inductive unit@{i} : Type@{i} := tt.
+
+Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n.
+Proof.
+intros m n P e p.
+abstract (rewrite e in p; exact p).
+Defined.
+
+Check foo_subproof@{Set Set}.
+
+Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n.
+Proof.
+intros m n P e p.
+abstract (rewrite e in p; exact p).
+Defined.
+
+Check bar_subproof@{Set Set Set}.