diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_002.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_002.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v index ba69f6b1..dba4d599 100644 --- a/test-suite/bugs/closed/HoTT_coq_002.v +++ b/test-suite/bugs/closed/HoTT_coq_002.v @@ -9,7 +9,7 @@ Section SpecializedFunctor. (* Variable objC : Type. *) Context `(C : SpecializedCategory objC). - Polymorphic Record SpecializedFunctor := { + Record SpecializedFunctor := { ObjectOf' : objC -> Type; ObjectC : Object C }. |