The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

On 20.03.2016 18:03, Jonathan Leivent wrote:
> How about inserting a hole where you might want the coercion:

I don't understand... I do *not* want a coercion unless I explicitly add
one.

Another example where this comes up in the actual development: We have a
dependent type of expressions (with the index in the type giving the
variables that may be free), and there is a function "wexpr" to weaken
that index. If I forgot to call wexpr e.g. in the definition of
substitution, I don't get an error -- instead, I get an unexpected and
unsolvable obligation. I then have to guess which of the many places
where expressions occur in the term caused is the culprit.

Kind regards,
Ralf