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?
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)
if you don't support SProp you can use Context.annotR
otherwise you need to get the relevance of the types
Thanks! Is there a place I can read more about this change?
Arpan Agrawal has marked this topic as resolved.
Last updated: Nov 29 2023 at 22:01 UTC