Process completed with exit code 1.

Makefile.coq:838: src/CLI.v

Makefile.coq:838: src/CLI.v

The following term contains unresolved implicit arguments: (fun (supported_languages : supported_languagesT) (machine_wordsizev : machine_wordsize_opt) '(((((((((((((((((((((((((((((((((((((((((((( ( ( ( langv, package_namev) as p44, class_namev) as p43, package_casev) as p42, class_casev) as p41, private_function_casev) as p40, public_function_casev) as p39, private_type_casev) as p38, public_type_casev) as p37, no_prefix_fiatv) as p36, staticv) as p35, internal_staticv) as p34, inlinev) as p33, inline_internalv) as p32, no_wide_intv) as p31, widen_carryv) as p30, widen_bytesv) as p29, no_selectv) as p28, split_multiretv) as p27, value_barrierv) as p26, no_primitivesv) as p25, no_field_element_typedefsv) as p24, emit_all_castsv) as p23, relax_primitive_carry_to_bitwidthv) as p22, cmovznz_by_mulv) as p21, shiftr_avoid_uint1v) as p20, only_signedv) as p19, hint_file_namesv) as p18, output_file_namev) as p17, asm_output_file_namev) as p16, asm_label_exact_matchv) as p15, asm_regv) as p14, asm_callee_saved_registersv) as p13, asm_stack_sizev) as p12, no_error_on_unused_asm_functionsv) as p11, asm_input_firstv) as p10, asm_reg_rtlv) as p9, asm_error_on_unique_names_mismatchv) as p8, asm_rewriting_pipelinev) as p7, asm_rewriting_passesv) as p6, asm_debug_symex_asm_firstv) as p5, doc_text_before_function_namev) as p4, doc_text_before_type_namev) as p3, doc_newline_before_package_declarationv) as p2, doc_newline_in_typedef_boundsv) as p1, doc_prepend_header_rawv) as p0, doc_prepend_headerv) as p, debugv) => let flag_to_bool := fun x : full_flag_status => bool_of_full_flag_status x false in let to_bool := fun ls : list (string * Arg.spec_data Arg.Unit) => (0 <? Datatypes.length ls)%nat in let to_string_list := fun ls : list (string * Arg.spec_data Arg.String) => List.map snd ls in let to_N_list := fun ls : list (string * (string * N)) => List.map snd (List.map snd ls) in let to_Z_flat_list := fun ls : list (string * (string * list Z)) => flat_map snd (List.map snd ls) in let to_reg_list := fun ls : list (string * (string * list REG)) => match List.map snd (List.map snd ls) with | [] => None | y :: l => Some (List.concat (y :: l)) end in let to_rewriting_pipeline_list := fun ls : list (string * (string * list rewrite_pass)) => match List.map snd (List.map snd ls) with | [] => default_rewrite_pass_order | y :: l => List.concat (y :: l) end in let to_assembly_callee_saved_registers_opt := fun ls : list (string * (string * assembly_callee_saved_registers_opt)) => choose_one_of_many (List.map (fun '(_, (_, v)) => v) ls) in let to_assembly_callee_saved_registers_default := fun (ls : list (string * (string * assembly_callee_saved_registers_opt))) (default : assembly_callee_saved_registers_opt) => Option.sequence_return (to_assembly_callee_saved_registers_opt ls) default in let to_N_opt := fun ls : list (string * (string * N)) => choose_one_of_many (to_N_list ls) in let to_N_default := fun (ls : list (string * (string * N))) (default : N) => Option.sequence_return (to_N_opt ls) default in let to_string_opt := fun ls : list (string * Arg.spec_data Arg.String) => choose_one_of_many (to_string_list ls) in let to_string_default := fun (ls : list (string * Arg.spec_data Arg.String)) (default : Arg.spec_data Arg.String) => Option.sequence_return (to_string_opt ls) default in let to_capitalization_data_opt := fun ls : list (string * (string * capitalization_data)) => choose_one_of_many (List.map (fun '(_, (_, v)) => v) ls) in let to_capitalization_convention_opt := fun ls : list (string * (string * capitalization_data)) => option_map (fun d : capitalization_data => {| capitalization_convention_data := d; only_lower_first_letters := true |}) (to_capitalization_data_opt ls) in let '((f, unknown_debug_options) as p45, (debug_on_successv, debug_rewritingv) as t) := parse_flag_opts special_debug_options known_debug_options (default_debug :: List.map snd debugv) in let default_asm_rewriting_pass_status := true in let '(unknown_asm_rewriting_passes, asm_rewriting_pass_filterv) := parse_flag_opts_to_bool_filter default_asm_rewriting_pass_status speci