From a59bdc4144476c0794ff24fc6180e21671842395 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Jul 2017 17:57:22 +0200
Subject: Removing the uses of abstraction-breaking code in Lemmas.

I had to slightly tweak a test in order to work around a bug of simpl that
loses universes constraints when refolding polymorphic fixpoints.
---
 test-suite/bugs/closed/HoTT_coq_123.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3