diff options
| -rw-r--r-- | test-suite/bugs/opened/3278.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_106.v | 5 |
2 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v index 2c6d391a0c..ced535afd5 100644 --- a/test-suite/bugs/opened/3278.v +++ b/test-suite/bugs/opened/3278.v @@ -1,5 +1,5 @@ Module a. - Fail Check let x' := _ in + Check let x' := _ in $(exact x')$. Notation foo x := (let x' := x in $(exact x')$). 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 |