Stream: Coq devs & plugin devs

Topic: ✔ Moving from Name.t to Context.binder_annot


view this post on Zulip Arpan Agrawal (Jul 25 2023 at 19:20):

In the following function (written initially in Coq 8.9), the input array is of type Name.t array, but from Coq 8.10 onwards, Context.Rel.Declaration (CRD below), the LocalAssum takes a Name.t Context.binder_annot as the first argument. Does this mean the type signature will need to be changed or is there another way to transform the array to the required type?
Thanks!

let bindings_for_fix (names : name array) (typs : types array) : rel_declaration list =
  Array.to_list
    (CArray.map2_i
       (fun i name typ -> CRD.LocalAssum (name, Vars.lift i typ))
       names typs)

view this post on Zulip Gaëtan Gilbert (Jul 25 2023 at 19:46):

if you don't support SProp you can use Context.annotR
otherwise you need to get the relevance of the types

view this post on Zulip Arpan Agrawal (Jul 25 2023 at 19:50):

Thanks! Is there a place I can read more about this change?

view this post on Zulip Notification Bot (Jul 25 2023 at 19:50):

Arpan Agrawal has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC