diff options
| author | Pierre-Marie Pédrot | 2018-10-04 11:10:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-04 11:10:50 +0200 |
| commit | 79da82da057224eec8abaf96c20b0725f18b2945 (patch) | |
| tree | 2a64cf563eb5f8d39e3fdfb4aa10053dd2e4f6ae /test-suite | |
| parent | 07ae306b9601653a6edbdefd1b3b5275439611bf (diff) | |
| parent | 8ef1be1aead0dbcc2d3cc46a7e5eaa02f9ad6069 (diff) | |
Merge PR #7361: Towards selecting "best" unification failure among several
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/unifconstraints.out | 8 | ||||
| -rw-r--r-- | test-suite/output/unifconstraints.v | 6 |
2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index ae84603622..2fadd747b7 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -63,3 +63,11 @@ unification constraint: True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = veeryyyyyyyyyyyyloooooooooooooonggidentifier +The command has indeed failed with message: +In environment +P : nat -> Type +x : nat +h : P x +Unable to unify "P x" with "?P x" +(unable to find a well-typed instantiation for "?P": cannot ensure that +"nat -> Type" is a subtype of "nat -> Prop"). diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v index b9413a4ac2..179dec3fb0 100644 --- a/test-suite/output/unifconstraints.v +++ b/test-suite/output/unifconstraints.v @@ -20,3 +20,9 @@ Goal forall n m : nat, True /\ True /\ True \/ 3:clear m. Show. Admitted. +Unset Printing Existential Instances. + +(* Check non regression of error message (the example can eventually + improve though and succeed) *) + +Fail Check fun P (x:nat) (h:P x) => exist _ x (h : P x). |