Closed herbelin closed 1 week ago
I think I prefer having the empty newline to separate the evars.
I think I prefer having the empty newline to separate the evars.
We could have something similar to the conversion mismatch error, that is, printing the reason after the environment:
In environment:
...
Unable to satisfy the following constraints:
?x : T
?x0 : T
[...] [...] |- t == u
and:
In environment:
...
Could not find an instance for the following existential variables:
?x : T
?x0 : T
??
(And incidentally adding a colon to In environment
in the conversion mismatch error.)
I mean the newline between evars, ie I prefer
?x : T
?x0 : T
rather than
?x : T
?x0 : T
@SkySkimmer:
But then why newlines between existential variables and not also between the (universal) variables of an environment?
Actually, and more generally, I wonder whether it would not be worth to always print the type and context of evars occurring in a goal. Say, that the following:
Goal forall x, exists y, forall z, z + y + x = x + z.
intro; eexists; intro.
Show.
gives:
x : nat
?y : nat
z : nat
============================
z + ?y + x = x + z
(possibly with extra context information when the evar derives by unification from a hole not in the current "spine" of the term)
We could have something similar to the conversion mismatch error, that is, printing the reason after the environment:
That indeed sounds better.
But then why newlines between existential variables and not also between the (universal) variables of an environment?
Because I want to quickly distinguish the failed constraints (which is harder when they're a wall of text), I don't need to quickly distinguish env variables.
@proux01, @SkySkimmer: I moved "In environment" before the main explanation and I restored the double newlines (though w/o the last trailing one).
@coqbot merge now
This PR is an attempt to get:
For instance, in an example I'm working on, it gives:
while it was before:
Maybe the context and list of evars should be more clearly separated?
Also, in a situation without proper constraints like this one:
the message is now:
while it was before:
This is to be compared to the case of only one remaining existential variable in a class:
Maybe the message for one or more unresolved evars could be merged actually?