coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to get a constr_expr?

From: Beta Ziliani <bziliani AT famaf.unc.edu.ar>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to get a constr_expr?
Date: Wed, 13 Apr 2016 11:14:50 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bziliani AT famaf.unc.edu.ar; spf=None smtp.mailfrom=bziliani AT famaf.unc.edu.ar; spf=None smtp.helo=postmaster AT famaf.unc.edu.ar
Ironport-phdr: 9a23:3dnqTx09bS6ajEk3smDT+DRfVm0co7zxezQtwd8ZsegRLvad9pjvdHbS+e9qxAeQG96Lu7QZ0KGI7ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6CyZnsnL7vs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOf7Ubl8azWm7q5tSVe8gjUGMz8w9mD/hMV1hawdvRSq4RFz3sjdetfGZ7JFYqrBcIZCFiJ6VcFLWnkEW9vkYg==

On Wed, Apr 13, 2016 at 11:04 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 13/04/2016 15:33, Beta Ziliani wrote:
> Actually, I think what I need is an open_constr. Now the question is,
> what do I do with the sigmas? I get one from the goal, and one for each
> open_constr, which one should I use, or how should I combined them?

You're using 8.5 I believe? This open_constr API is quite broken and is
a source of evar leaks, but there is nothing better in that version.
AFAIR, the sigma you get in the open_constr argument is an extension of
the one of the goal, so that you can discard the latter...

Mmm... Not quite. I have two open_constrs c and c' with sigmas s and s'. It looks like in s there are no evars from c' and viceversa :-(

PMP

Re: [Coq-Club] How to get a constr_expr?, Beta Ziliani, 04/13/2016
- Re: [Coq-Club] How to get a constr_expr?, Pierre-Marie Pédrot, 04/13/2016
  - Re: [Coq-Club] How to get a constr_expr?, Beta Ziliani, 04/13/2016
    - Re: [Coq-Club] How to get a constr_expr?, Pierre-Marie Pédrot, 04/13/2016
      - Re: [Coq-Club] How to get a constr_expr?, Beta Ziliani, 04/13/2016
        
        Re: [Coq-Club] How to get a constr_expr?, Matthieu Sozeau, 04/13/2016
        
        Re: [Coq-Club] How to get a constr_expr?, Beta Ziliani, 04/13/2016
        
        Re: [Coq-Club] How to get a constr_expr?, Beta Ziliani, 04/13/2016