diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_098.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_098.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_098.v b/test-suite/bugs/opened/HoTT_coq_098.v index 1e7be20d5f..a07f2f0fa2 100644 --- a/test-suite/bugs/opened/HoTT_coq_098.v +++ b/test-suite/bugs/opened/HoTT_coq_098.v @@ -62,8 +62,8 @@ End failure. Module polycontext. Section SpecializedFunctor. - Polymorphic Context `(C : @SpecializedCategory objC). - Polymorphic Context `(D : @SpecializedCategory objD). + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). Polymorphic Record SpecializedFunctor := { |