diff options
| author | Hugo Herbelin | 2019-12-23 20:22:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-23 22:52:29 +0100 |
| commit | 18626b09a8a8ea1d56a7f91f347e1ebb3960e2c6 (patch) | |
| tree | e2480d799590b4411406bdec884c8adcc8625f97 /test-suite | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.
Might be improvable further. In the first example, we have two
environments involved and one is implicit. It does not seem excluded
that a variable name of the second environment shows up which is not
listed in the first environment.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/unification.out | 11 | ||||
| -rw-r--r-- | test-suite/output/unification.v | 12 |
2 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out new file mode 100644 index 0000000000..dfd755da61 --- /dev/null +++ b/test-suite/output/unification.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +In environment +x : T +T : Type +a : T +Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate +"?X" because "T" is not in its scope: available arguments are +"x" "C a"). +The command has indeed failed with message: +The term "id" has type "ID" while it is expected to have type +"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope). diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v new file mode 100644 index 0000000000..ff99f2e23c --- /dev/null +++ b/test-suite/output/unification.v @@ -0,0 +1,12 @@ +(* Unification error tests *) + +Module A. + +(* Check regression of an UNBOUND_REL bug *) +Inductive T := C : forall {A}, A -> T. +Fail Check fun x => match x return ?[X] with C a => a end. + +(* Bug #3634 *) +Fail Check (id:Type -> _). + +End A. |