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

…rsive.
mattam82 · Mar 6, 2024 · 497abdf · 497abdf
1 parent 7296932
commit 497abdf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/splitting.ml b/src/splitting.ml
@@ -455,8 +455,8 @@ let define_mutual_nested env evd get_prog progs =
     in
     let names, tys, bodies = nf_fix !evd (names, tys, bodies) in
     try
-      Pretyping.search_guard env (Array.to_list possible_indexes)
-          (names, tys, bodies)
+      Option.get (Pretyping.search_guard env (false, Array.to_list possible_indexes)
+          (names, tys, bodies))
     with e -> 
       user_err_loc ((fst (List.hd progs)).program_loc, CErrors.print e)
   in