diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_106.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_106.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_106.v b/test-suite/bugs/opened/HoTT_coq_106.v index 8d36abc0ed..a566459546 100644 --- a/test-suite/bugs/opened/HoTT_coq_106.v +++ b/test-suite/bugs/opened/HoTT_coq_106.v @@ -8,9 +8,10 @@ Instance ispointed_forall `{H : forall a : A, IsPointed (B a)} : IsPointed (forall a, B a) := fun a => @point (B a) (H a). -Fail Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))} +Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))} : IsPointed (sigT B). -(* Toplevel input, characters 20-108: +(* Message was at some time: +Toplevel input, characters 20-108: Error: Unable to satisfy the following constraints: UNDEFINED EVARS: ?8==[A H B |- IsPointed (forall x : Type, ?13)] (parameter IsPointed of |