diff options
| author | Hugo Herbelin | 2014-12-05 14:13:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-05 17:55:32 +0100 |
| commit | 8bf7221667dc2868027ed1080b3b70fd66144309 (patch) | |
| tree | 16be9e4ff0947b1c2232ad52676e6a6e767faa71 | |
| parent | 11919074c08a64e78e5a5581d744332a093850f0 (diff) | |
Commits on evar-evar unification fixed HoTT_coq_106 and improved the
status of #3278 (more precisely, it fixed a bug visible in the #3278
report, but a bug which arrived after #3278 was submitted).
| -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 |