Jasmin.Bigoptype __ = Obj.tval applybig : ('a1, 'a2) bigbody -> 'a1 -> 'a1val reducebig : 'a1 -> 'a2 list -> ('a2 -> ('a1, 'a2) bigbody) -> 'a1module type Coq_bigop_Locked = sig ... endmodule Coq_bigop : Coq_bigop_Lockedval index_enum : Fintype.Finite.coq_type -> Fintype.Finite.sort list