coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to get a constr_expr?

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] How to get a constr_expr?
Date: Mon, 7 Mar 2016 16:20:18 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:Dl767xzskzmcgBjXCy+O+j09IxM/srCxBDY+r6Qd0ewRIJqq85mqBkHD//Il1AaPBtWEraIdwLOM6ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZTunLnootX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjcQKw9EQaj66ZiTh6g3C0KKzcR9XnWz9dvl+Rcuh339E83+JLdfIzAbKk2RajaZ95PADMZBss=

Hi all,

Say I have a plugin with a procedure "f" that processes a constr_expr, and I want to write a tactic for it. I can't write the following:

TACTIC EXTEND myf
| [ "myf" constr_expr(c) ] -> [ f c ]

Is there an argument for a constr_expr? Or should I change "f" to get an object of a distinct type? f uses Proofview, and the idea is to interpret c in the evarmap provided by the proofview.

Thanks,

Beta

[Coq-Club] How to get a constr_expr?, Beta Ziliani, 03/07/2016
- Re: [Coq-Club] How to get a constr_expr?, Pierre-Marie Pédrot, 03/07/2016