The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/20/2016 02:10 PM, Ralf Jung wrote:
> 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.

I guess I misunderstood you then.  I thought you had a coercion from tt 
7 to tt 5, but obviously not from 7 to 5.

> 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

I actually don't use Program for various reasons, different from the 
ones you listed.  I have better control over refine in proof mode.

-- Jonathan