diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_056.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_056.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index 3e3a987a7c..b80e0bb0e4 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn} Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}. Global Instance FunctorApplicationDash C D (F : Functor C D) -: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0. +: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}. Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B) -: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100. +: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}. Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope. |