The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

https://coq.github.io/doc/master/api/coq/Library/index.html#val-indirect_accessor

Gaëtan Gilbert

On 02/07/2020 19:04, Francisco Trucco wrote:
> Hi coq-club!
>
> We are currently implementing a Coq plugin that makes use of the
> Coq API <https://coq.github.io/doc/master/api/coq>. 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 
> <https://coq.github.io/doc/master/api/coq/Declarations/index.html#type-constant_def>
>  to a constr 
> <https://coq.github.io/doc/master/api/coq/Constr/index.html#type-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 
> <https://coq.github.io/doc/master/api/coq/Opaqueproof/index.html#val-force_proof> 
> now takes an indirect_accessor 
> <https://coq.github.io/doc/master/api/coq/Opaqueproof/index.html#type-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