sig val generate_coq_decidable_equality : 'a list -> Typed_ast.name_l -> Typed_ast.texp -> Output.t end