diff options
| author | Hugo Herbelin | 2018-04-26 15:51:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 14:21:10 +0200 |
| commit | 8ef1be1aead0dbcc2d3cc46a7e5eaa02f9ad6069 (patch) | |
| tree | 60e562a2662a8a499c359c2454a37425d217b1c7 /test-suite | |
| parent | cfefed1cb20b6abe33c222df49d346867bafbc7f (diff) | |
Unification failure: don't give preference to a "beyond capabilities" error.
This is actually a bit ad hoc at this stage in the sense that this is
specifically to prefer an informative first-order unification failure
over the currently always uninformative failure coming from
second-order unification.
When second-order unification shall be able to give more information,
one may consider alternative strategies, even maybe reporting not just
one but the list of failures in all (interesting) branches.
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). |