Commit fe00489
File tree
- src
- tests
- basics
- ack
- binomial_heap
- bool_ops
- closures_in_data
- colist
- comparison
- cotree
- currying
- doc_comments
- eq_ord_show
- graph
- higher_order
- int63_arith
- lambda
- levenshtein
- list
- module
- multi_ind_functor
- mutual_functor
- mutual_mod
- mutual_recursion
- n_gmp
- n_int
- nat_gmp
- nat
- option
- prim_array
- prim_float
- record_match
- regexp
- sections
- sigma_types
- sort
- stream
- string_match
- sum
- tail_rec_map
- tail_rec_rev
- tail_rec_zip
- tokenizer
- topological_sort
- tree
- typeclasses
- typed_expr
- z_gmp
- z_int
- monadic
- bind_type_inference
- free_monad
- io
- itree_effects
- itree_reified
- monadic
- mutable_vector
- parallel
- skiplist
- stm_hash_map
- stm
- thread
- regression
- accum_closure_capture
- add_one
- anon_fixpoint
- axiom_types
- bank_lookup_default
- bcd_digit_upper_bound
- binary_nums
- bind_eta_reduced
- block_template_edge
- block_template_hygiene
- block_template_nonlocal
- block_template_semicolon
- block_template_stress
- block_template_types
- bool_dec_bde
- bool_dec_std
- canon_struct
- clock
- closure_capture_match
- closure_chain
- closure_escape_match
- closure_in_ctor
- closure_let_escape
- closure_map_escape
- closure_nested_escape
- closure_pair_this
- closure_recursive_build
- coalition_bid_honor_trace
- coercions
- cofix_this_thunk
- coind_guard
- coinductive
- comprehensive_patterns
- computational_proof
- constrained_poly
- constructor_bugs
- count_down
- count_loop_test_target
- cps_closure_chain
- cps_escape
- cps
- cpu_emulator
- crane_move_hunt
- ctor_escape_collision
- custom_inline_bug
- decode_list
- deep_app
- deep_destruct
- deep_map
- deep_patterns
- deep_pattern
- density_potential_trace
- dep_elim
- dep_record
- dependent_elim_stdexcept_probe
- dependent_template_stress
- dependent_typename
- dim10_tower_proof_chain
- dir
- disassemble_ops
- double_invoke_move
- double_opposite_witnesses
- drop_head_default
- effect_bare_void
- effect_bind_action
- effect_complex_args
- effect_complex_return
- effect_compose
- effect_cross_module
- effect_deep_compose
- effect_dir_path
- effect_getline_stress
- effect_higher_order
- effect_hof_void
- effect_list_return
- effect_match_arg
- effect_nested_io
- effect_option_match
- effect_option_string
- effect_poly
- effect_recursive_list
- effect_unit_stress
- effect_workflow
- embed_effect
- empty_match
- empty_system_bank_count
- encode_ops
- enum_switch_qualified
- env
- epoch_cell_glyph_trace
- equations
- erased_record
- escape_collision
- even_length_byte_validation
- extract_directives
- fetch_ops
- fim_operates_on_pairs
- fin_operates_on_pairs
- fix_capture_fn_arg
- fix_chain_build
- fix_compose_escape
- fix_curried_escape
- fix_direct_return
- fix_escape_capture
- fix_escape_match
- fix_fold_escape
- fix_higher_order
- fix_in_record
- fix_move_capture
- fix_pair_two_closures
- fix_partial_app
- fix_via_simple_lambda
- fold_closure_accum
- fold_closure_build
- fold_sequence_state_trace
- forall_list
- forward_spec_ascii
- func_only_submodule_ab
- function_return_branch_probe
- function_vernac
- functor_comp
- functor_output_probe
- get_pair_bound_prop
- higher_kinded
- higher_rank_argument_probe
- historical_event_safety_trace
- hof_closure_escape
- hof_tree_loopify
- identifier_escape_param
- iife_name_clash
- implicit_args
- imported_alias_qualification
- inc_xch_nibble
- ind_param
- inductive_in_module
- init_state_props
- instruction_classifiers
- instruction_cycles
- instruction_sequence_exec
- isz_ops
- jcn_ops
- jin_uses_pair_for_jump
- jms_bbl_roundtrip
- jump_targets
- kbp_multibit_default
- keyword_class_global
- large_enum
- large_mutual
- let_closure_escape
- let_fix
- let_in
- let_match_type2
- let_match_type
- let_pair_shadow
- list_closure_escape
- load_program_head_write
- load_program
- local_fix_higher_order_probe
- loop_body_iteration
- loopify_advanced_lists
- loopify_advanced_patterns
- loopify_algorithms
- loopify_classics
- loopify_coind_colist
- loopify_coind_stream
- loopify_combinatorics
- loopify_comparators
- loopify_decltype
- loopify_expr_variants
- loopify_expr
- loopify_extrema
- loopify_folds
- loopify_generators
- loopify_grouping
- loopify_hofs
- loopify_itree_reified
- loopify_itree_seq
- loopify_list_access
- loopify_list_combining
- loopify_list_generation
- loopify_list_generators
- loopify_list_of_lists
- loopify_list_pairing
- loopify_list_relations
- loopify_list_subsequences
- loopify_list_transforms
- loopify_list_windows
- loopify_lists
- loopify_match_arg
- loopify_more_trees
- loopify_multi_recursion
- loopify_nested_constructs
- loopify_numbers
- loopify_numeric_misc
- loopify_numeric_sequences
- loopify_option_maybe
- loopify_option
- loopify_pairs
- loopify_patterns
- loopify_polymorphic
- loopify_predicates
- loopify_scans
- loopify_search_opt
- loopify_search
- loopify_sequences
- loopify_sorting
- loopify_special_recursion
- loopify_strings
- loopify_structures
- loopify_tail
- loopify_tmc
- loopify_tree_paths
- loopify_tree_variants
- loopify_trees
- lowercase_eponymous_record
- main_entrypoint
- main_toplevel
- map_partial_app
- match_closure_escape
- match_ctor_closure
- match_fallback_nat
- match_monadic
- match_ref_after_move
- mergesort_fuel
- method_partial_app
- modpath_escape_collision
- module_type_name_clash_probe
- modulo_wrap
- monadic_closure
- monadic_void_edge
- move_capture_reuse
- move_safety
- mutual_coind
- mutual_fix_escape
- mutual_indexed
- mutual_record
- mutual_recursion
- name_clash_binding_reuse
- name_clash_ctor_field
- name_clash_iife_this
- name_clash_let_match
- name_clash_match_match
- name_clash_nested_deep
- name_clash_return_this
- name_clash_scope_leak
- name_clash_scrutinee
- nat_mod_zero
- nested_ind
- nested_match_closure
- nested_mod
- nested_partial_app
- nested_record_update_qual
- nested_tree
- numeral_edge
- numeral_stress
- opaque
- opcode_operand_decode
- opposite_property_transfer_trace
- option_closure_escape
- option_let_none_bug
- option_some_escape
- page_address
- page_ops
- pair_closure_escape
- partial_app_move
- partial_apply
- pathological_record
- path
- pattern_impossible
- pendant_sumtree_roundtrip
- ping_pong
- poly_inductive
- polygon_winding_area_trace
- polymorphic_function_field_probe
- polymorphic_helper
- port_write_nibble_mask
- preserves_all_pairs
- prim_array_ops
- prim_proj
- primitive_rec_typeclass
- program_fixpoint
- program_targets_region_scan
- program_wf_prop
- program_wf
- prom_ops
- prop_erasure
- pstring
- pulse_parse_certificate
- qualified_record_shadow
- qualified_shadow_ascii
- ram_accessor
- ram_bad_state
- ram_empty_wf
- ram_init_reset
- ram_ops
- ram_state_ops
- ram_write
- rdr_reads_from_selected_port
- read_variable_capture
- rec_record
- record_apply
- record_case_body
- record_closure_escape
- record_defaults
- record_erased_proof_fields
- record_field_patterns
- record_function_field_stdlib_probe
- record_proj
- record_use_after_move
- recursive_monadic
- region_membership_bounds
- region_patch_write
- register_pair_ops
- reset_state
- reuse_alias
- reuse_fn_in_body
- reuse_lambda_capture
- reuse_mixed_fields
- reuse_move_shadow
- reuse_scrutinee
- reuse_self_cycle
- reuse_tag_mismatch
- reuse_use_after_move
- rocq_bug_10757
- rocq_bug_10796
- rocq_bug_11114
- rocq_bug_13453
- rocq_bug_13581
- rocq_bug_14100
- rocq_bug_14174
- rocq_bug_14843
- rocq_bug_16288
- rocq_bug_20894
- rocq_bug_20989
- rocq_bug_3923
- rocq_bug_4616
- rocq_bug_4709
- rocq_bug_4710
- rocq_bug_4720
- rocq_bug_4844
- rocq_bug_5177
- rocq_bug_7228
- sections_modules
- set_cur_bank_modulo
- set_test_pin_update
- setoid_rw
- shadow_qual_node
- sigma_assert
- signature_parity_fix
- sigt_probe
- simple_lambda_field_capture
- singleton_record
- sprop
- src_uses_pair_value
- src_wrr_rom_port_roundtrip
- src_wrr_updates_rom_port
- stack_ops
- step_fetch_decode_exec
- steps_counter_unroll
- superfluous_moves
- tailrec_reorder_probe
- temp_file
- this_capture_dangling
- this_capture_record
- timing_preserves_wf_simple
- todo_dependent_field_alias
- todo_erased_instance_param
- todo_explicit_type_app_alias
- todo_extract_constant_noninline
- todo_inline_custom_poly_id
- todo_inline_custom_symbol
- todo_letin_applied_poly
- todo_monadic_global_alias
- todo_nested_module_type_functor
- todo_nested_module_type
- todo_polymorphic_erased_helper
- todo_type_app_instance_alias
- todo_type_subst_pack_alias
- todo_with_module_constraint
- todo_with_type_constraint
- tuple
- type_app
- type_indexed_inductive_probe
- typeclass_function_field_probe
- typeclass_method_function_return_probe
- unit_monostate_erase
- unit_type
- unit_void_edge2
- unit_void_edge
- unit_void_stress
- universe_poly
- unsound_axioms
- update_nth_bounds
- use_after_move
- valid_layout_window
- valid_program_byte_reject
- valid_program_checks
- validated_pump_delivery_trace
- validated_virtual_crossmatch_trace
- value_type_match_fix
- visit_match_bug
- void_callback
- well_founded_rec
- where_clause
- wpm_ops
- wrapper_collision_pos
- wrapper_decl_merge
- wrm_then_rdm_reads_back
- wrr_preserves_other_ports
- wrr_rdr_roundtrip
- z_overflow
- wip
- accum_closure_escape
- dependent_return_unit_probe
- existential_closure_probe
- loopify_unit_void_repro
- no_mapping_event_probe
- z_abs_min
- z_arith_overflow
- z_div_min
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
772 | 772 | | |
773 | 773 | | |
774 | 774 | | |
| 775 | + | |
| 776 | + | |
775 | 777 | | |
776 | 778 | | |
777 | 779 | | |
| |||
807 | 809 | | |
808 | 810 | | |
809 | 811 | | |
810 | | - | |
| 812 | + | |
811 | 813 | | |
| 814 | + | |
| 815 | + | |
| 816 | + | |
| 817 | + | |
| 818 | + | |
| 819 | + | |
812 | 820 | | |
813 | 821 | | |
814 | 822 | | |
815 | 823 | | |
816 | | - | |
| 824 | + | |
| 825 | + | |
| 826 | + | |
| 827 | + | |
| 828 | + | |
817 | 829 | | |
818 | 830 | | |
| 831 | + | |
| 832 | + | |
| 833 | + | |
| 834 | + | |
| 835 | + | |
| 836 | + | |
| 837 | + | |
| 838 | + | |
819 | 839 | | |
820 | 840 | | |
821 | 841 | | |
| |||
849 | 869 | | |
850 | 870 | | |
851 | 871 | | |
852 | | - | |
| 872 | + | |
| 873 | + | |
| 874 | + | |
| 875 | + | |
| 876 | + | |
| 877 | + | |
853 | 878 | | |
854 | 879 | | |
| 880 | + | |
| 881 | + | |
855 | 882 | | |
856 | 883 | | |
857 | 884 | | |
| |||
0 commit comments