diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 17:57:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-13 18:19:09 +0200 |
| commit | a59bdc4144476c0794ff24fc6180e21671842395 (patch) | |
| tree | ee175002ae8197c9a94e5ec3fcdaeeededbb4f04 /test-suite | |
| parent | f2a01d400c92c48caf79771f17820a492f99057b (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_123.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index cd9cad406..7bed956f3 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. |