diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_014.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_014.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index 5c45036643..35f8701b2f 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -200,3 +200,4 @@ Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) ( Morphism (FunctorCategory GraphIndexingCategory TypeCat) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*) Proof. Admitted. +End test. |