Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Gradual use of Program

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Gradual use of Program


Chronological Thread 
  • From: Matthieu Sozeau <mattam AT mattam.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Gradual use of Program
  • Date: Fri, 25 Mar 2016 00:13:16 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
  • Ironport-phdr: 9a23:vLdcYBV6GxpMZ3UwZBSrX8v9MQ7V8LGtZVwlr6E/grcLSJyIuqrYZheBt8tkgFKBZ4jH8fUM07OQ6PCwHzVRqszZ+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VOlQD3mL1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDtxNUHwjE4QyyZZDjvyLn/r540TWGNMjeSLkoRT2nqaBxR0m72288Kzcl/TSP2YRLh6VBrUf5qg==

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




Archive powered by MHonArc 2.6.18.

Top of Page