The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Ralf,

  it's certainly possible and quite trivial to disable this feature,

you're right that it can get pretty unwiedly, I'll get on it.

Best regards,

-- Matthieu

On Sun, Mar 20, 2016 at 7:34 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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