diff options
| author | Pierre-Marie Pédrot | 2019-12-29 17:23:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-29 17:23:34 +0100 |
| commit | e176bb419256580d53749d72d533914f794a981d (patch) | |
| tree | a28883cc47f315e8c264db21f05fa32536d8fb18 /test-suite | |
| parent | 99b064d1079f62bdabfd7374ae77246828e8b08d (diff) | |
| parent | 18626b09a8a8ea1d56a7f91f347e1ebb3960e2c6 (diff) | |
Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message
Reviewed-by: ppedrot
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. |