Skip to content

Commit

Permalink
Adapt to search_guard, now able to decide late if recursive or corecu…
Browse files Browse the repository at this point in the history
…rsive.
  • Loading branch information
herbelin committed Apr 11, 2024
1 parent 6010562 commit ee07d8d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/splitting.ml
Original file line number Diff line number Diff line change
Expand Up @@ -449,7 +449,7 @@ let define_mutual_nested env evd get_prog progs =
let possible_indexes =
Array.map3 (compute_possible_guardness_evidences !evd) structargs bodies tys
in
Pretyping.esearch_guard env !evd (Array.to_list possible_indexes)
Pretyping.esearch_guard env !evd (false, Array.to_list possible_indexes)
(names, tys, bodies)
in
let declare_fix_fns i (p,prog) =
Expand Down

0 comments on commit ee07d8d

Please sign in to comment.