diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_064.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_064.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v index b4c745375..d02a5f120 100644 --- a/test-suite/bugs/closed/HoTT_coq_064.v +++ b/test-suite/bugs/closed/HoTT_coq_064.v @@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C) Generalizable All Variables. Axiom fs : Funext. +Existing Instance fs. Section bar. |