diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_106.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_106.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_106.v b/test-suite/bugs/opened/HoTT_coq_106.v index d3ef9f58c3..8d36abc0ed 100644 --- a/test-suite/bugs/opened/HoTT_coq_106.v +++ b/test-suite/bugs/opened/HoTT_coq_106.v @@ -8,7 +8,7 @@ Instance ispointed_forall `{H : forall a : A, IsPointed (B a)} : IsPointed (forall a, B a) := fun a => @point (B a) (H a). -Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))} +Fail Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))} : IsPointed (sigT B). (* Toplevel input, characters 20-108: Error: Unable to satisfy the following constraints: |