diff options
| author | Matthieu Sozeau | 2014-06-16 12:14:50 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-16 18:21:27 +0200 |
| commit | 636782e3aef984e9d57681d14c4cae5629e4a2d8 (patch) | |
| tree | 7261d078cd527eddc8b605fb7e7cf5291f76a4ad | |
| parent | 7e69422ea16c9e323d02fdd7c4927750b40bd2cf (diff) | |
HoTT bug #29 is fixed, using the correct notion of polymorphic product types.
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_029.v (renamed from test-suite/bugs/opened/HoTT_coq_029.v) | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_029.v b/test-suite/bugs/closed/HoTT_coq_029.v index 57f3fd22cf..4fd54b5699 100644 --- a/test-suite/bugs/opened/HoTT_coq_029.v +++ b/test-suite/bugs/closed/HoTT_coq_029.v @@ -164,6 +164,11 @@ Module SecondComment. Set Universe Polymorphism. Generalizable All Variables. + Record prod (A B : Type) := pair { fst : A; snd : B }. + Arguments fst {A B} _. + Arguments snd {A B} _. + Infix "*" := prod : type_scope. + Notation " ( x , y ) " := (@pair _ _ x y). Record Category (obj : Type) := Build_Category { Object :> _ := obj; @@ -301,15 +306,15 @@ Module SecondComment. Definition CommaCategoryProjection : Functor (CommaCategory S T) (ProductCategory A B). Admitted. - Fail Definition CommaCategoryProjectionFunctor_ObjectOf - : @SliceCategoryOver _ LocallySmallCat (ProductCategory A B : Category _) + Definition CommaCategoryProjectionFunctor_ObjectOf + : @SliceCategoryOver _ LocallySmallCat (ProductCategory A B) := existT _ - ((CommaCategory S T : Category _) : Category', tt) + ((CommaCategory S T) : Category', tt) (CommaCategoryProjection) : CommaCategory_ObjectT (IdentityFunctor _) (SliceCategory_Functor LocallySmallCat - (ProductCategory A B : Category _)). + (ProductCategory A B)). (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *) (* Toplevel input, characters 110-142: Error: |