Adapt to search_guard, now able to decide late if recursive or corecu…

…rsive.
mattam82 · Apr 13, 2024 · 3c778e0 · 3c778e0
1 parent 6010562
commit 3c778e0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/splitting.ml b/src/splitting.ml
@@ -449,8 +449,8 @@ 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)
-      (names, tys, bodies)
+    Option.get (Pretyping.esearch_guard env !evd (false, Array.to_list possible_indexes)
+      (names, tys, bodies))
   in
   let declare_fix_fns i (p,prog) =
     let newidx = indexes.(i) in