coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac and constr arguments with holes

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Ltac and constr arguments with holes
Date: Sun, 9 Nov 2014 19:28:01 -0500

On Sun, Nov 9, 2014 at 7:21 PM, Jonathan <jonikelee AT gmail.com> wrote:

So that undocumented open_constr has been around at least since 8.4? Sigh.

Indeed. For more fun, it behaves differently in 8.4-8.4pl3, and 8.4pl4-trunk: in 8.4-8.4pl3, it does typeclass resolution. In 8.4pl4-trunk, it does not do typeclass resolution. In 8.4pl4-8.4pl5, there is an open_constr_wTC that does typeclass resolution (there is no such thing in trunk).

[Coq-Club] Ltac and constr arguments with holes, Robbert Krebbers, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Arnaud Spiwack, 11/06/2014
  - Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
    - Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
      - Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
        
        Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Robbert Krebbers, 11/10/2014
  - Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/10/2014
    - Re: [Coq-Club] Ltac and constr arguments with holes, Jason Gross, 11/10/2014