coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to translate the body of a constant to a constr?

From: Francisco Trucco <franciscoctrucco AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to translate the body of a constant to a constr?
Date: Thu, 2 Jul 2020 19:04:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=franciscoctrucco AT gmail.com; spf=Pass smtp.mailfrom=franciscoctrucco AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f54.google.com
Ironport-phdr: 9a23:TzEG3hVJXN+apJk/heG5fuC5fzbV8LGtZVwlr6E/grcLSJyIuqrYbRCFt8tkgFKBZ4jH8fUM07OQ7/m+HzRcqs/Z6DhCKMUKC0ZYz51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6osyxbFuGdEdutZyW91OV6fgwv36sOs8JJ+6ShdtO8t+s5aXanmY6g0SKFTASg7PWwy+MDlrwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCNGH428cpAPD/IfMulEs4nzqVwOrR6kCgmtAuPk1ztEi3Dy0KE/1ekqDAPI0xE6H98Wv3varNv7OqQPX+6r0KbF1i/MY+9M1Drn9ITEbhIsrPeRVrxwa8rRzkwvGhvFgFWKs4PlOS+a1uUWs2eH6OprSPyhi3Q6qw5tvjevwdonh47HhoIP0F/E8zl2wIcuJdKkT050fcKkEIFNty6GK4R2RdgvQ25tuCkgy70GvYS3czQNyJQi3hPSbeGMfIeU7Bz5TumRPSt4i2x/eLK5nxu/70atx+LgW8SozltHoTRIn9rDuH4NyRDe9siKRud580ql2zuC2ADe5+BKL00wiabWKp4sz7oum5cSsEnOHy/4lUPrh6GYcUUk//Kn6+XhYrj+qZ+cNpN0igHjMqs1gMC/AOM4Pw4TVGaY4eSxzKPv8VH9TblQjfA7krPVvI7HKckZvKK0AwBY34A+4BilFTimys4XnXwfIVJFZh2Hi4/pNknLIP/iDPe/h02gkClwx/zbJ7HhDJXAI3fZnLfuerZ97EFcyA4twtxF+51UDbQBLOryWk/3qtPYEgc0PxKoz+vjEtlw1YMTVXiRDqOEMq7eq1+F6+03L+mJfoAVuTL9K/Y/5/7piH80gVEdfbOz0psRdH+4H+9mLFmeYXXwntcBC3oKsRYiQ+ztk1CCXjtTaGyzX6I4/D00FIWmDYLbSoC3nLOBxDu7HoFRZm1eFl+MFm7oe5yYVPcIdSKdOdRskicEVLikU48uzwuitA78y7p9L+rb4DcUtZz51Is92+qGnhYrsDdwEs610meXTmgykHlbaSUx2fVRu0V7wVaY2q8wv+ZFHtdUr6dHSA48Pp/HxOtxF8rvUQnGVtiMQVeiBN6hBGdiHZoK39YSbhMlSJ2ZhRfZ0n/2UuZExYzOP4Q99+fn51a0Is98z3jc06x41gspR8JOMSutgastrlGOVb6MqF2QkuORTYpZ3CPJ8z3en2+HvUUdThUpFKuYATYQYUzZqdm/7UTHHef3VeYXdzBZwMvHEZNkL8XzhAwfFvjmMdXaJWm2njXoCA==

Hi coq-club!

We are currently implementing a Coq plugin that makes use of the

Coq API. When we started working on the project we were using

Coq 8.9. We are now updating the Plugin to Coq 8.11 and we were

wondering how to translate the body of a constant to a constr.

This works in Coq 8.9 but it doesn't on Coq 8.11:

match cn.Declarations.const_body with
| Declarations.Undef _ ->
None
| Declarations.Def d ->
Some (Mod_subst.force_constr d)
| Declarations.OpaqueDef o ->
Some (Opaqueproof.force_proof (Global.opaque_tables ()) o)

In particular, force_proof now takes an indirect_accessor.

How do we obtain this indirect_accessor?
And what is the correct way to translate the body of a constant

to a constr?

Thank you in advance for your help!

Best,

Francisco Carlos Trucco Dalmas

[Coq-Club] How to translate the body of a constant to a constr?, Francisco Trucco, 07/02/2020
- Re: [Coq-Club] How to translate the body of a constant to a constr?, Gaëtan Gilbert, 07/02/2020