diff --git a/dev/ci/user-overlays/19107-herbelin-master+unify-fixpoint-cofixpoint-execution-paths.sh b/dev/ci/user-overlays/19107-herbelin-master+unify-fixpoint-cofixpoint-execution-paths.sh
new file mode 100644
index 000000000000..cc69b7213572
--- /dev/null
+++ b/dev/ci/user-overlays/19107-herbelin-master+unify-fixpoint-cofixpoint-execution-paths.sh
@@ -0,0 +1,2 @@
+overlay coq_lsp https://github.com/herbelin/coq-lsp main+adapt-coq-pr19107-merge-fixpoint-cofixpoint 19107 herbelin-master+unify-fixpoint-cofixpoint-execution-paths
+overlay autosubst_ocaml https://github.com/herbelin/autosubst-ocaml master+adapt-coq-pr19107-merge-fixpoint-cofixpoint 19107 herbelin-master+unify-fixpoint-cofixpoint-execution-paths
diff --git a/interp/constrexpr.mli b/interp/constrexpr.mli
index 0e5d7c8bc8b1..3b889e95db35 100644
--- a/interp/constrexpr.mli
+++ b/interp/constrexpr.mli
@@ -183,17 +183,17 @@ and branch_expr =
 
 and fix_expr =
   lident * relevance_info_expr
-  * recursion_order_expr option *
+  * fixpoint_order_expr option *
   local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
     lident * relevance_info_expr * local_binder_expr list * constr_expr * constr_expr
 
-and recursion_order_expr_r =
+and fixpoint_order_expr_r =
   | CStructRec of lident
   | CWfRec of lident * constr_expr
   | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
-and recursion_order_expr = recursion_order_expr_r CAst.t
+and fixpoint_order_expr = fixpoint_order_expr_r CAst.t
 
 (* Anonymous defs allowed ?? *)
 and local_binder_expr =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a3f4ccdbf184..4aa65b810a32 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -196,7 +196,7 @@ module Constr :
     val open_binders : local_binder_expr list Entry.t
     val one_open_binder : kinded_cases_pattern_expr Entry.t
     val one_closed_binder : kinded_cases_pattern_expr Entry.t
-    val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t
+    val binders_fixannot : (local_binder_expr list * fixpoint_order_expr option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
     val arg : (constr_expr * explicitation CAst.t option) Entry.t
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index f6d9a0c92076..591e4964c1ca 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -173,14 +173,12 @@ let () =
 
 let is_proof_termination_interactively_checked recsl =
   List.exists (function
-  | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } }
-      | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true
-  | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } }
-  | _, Vernacexpr.{ rec_order = None } -> false) recsl
+  | _, ( Some { CAst.v = (CMeasureRec _ | CWfRec _) }, _ ) -> true
+  | _, ( ( Some { CAst.v = CStructRec _ } | None), _) -> false) recsl
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacSynPure (VernacFixpoint(NoDischarge, List.map snd recsl))}))
+    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacSynPure (VernacFixpoint(NoDischarge, List.split (List.map snd recsl)))}))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
@@ -213,11 +211,11 @@ VERNAC COMMAND EXTEND Function STATE CUSTOM
     if is_interactive recsl then
       Vernactypes.vtopenproof (fun () ->
           CWarnings.with_warn warn
-            Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+            Gen_principle.do_generate_principle_interactive (List.split (List.map snd recsl)))
     else
       Vernactypes.vtdefault (fun () ->
           CWarnings.with_warn warn
-            Gen_principle.do_generate_principle (List.map snd recsl))
+            Gen_principle.do_generate_principle (List.split (List.map snd recsl)))
   }
 END
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a519d557b2b7..b34207c00f53 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -152,24 +152,14 @@ and rebuild_nal aux bk bl' nal typ =
 
 let rebuild_bl aux bl typ = rebuild_bl aux bl typ
 
-let recompute_binder_list fixpoint_exprl =
-  let fixl =
-    List.map
-      (fun fix ->
-        Vernacexpr.
-          { fix with
-            rec_order =
-              ComFixpoint.adjust_rec_order ~structonly:false fix.binders
-                fix.rec_order })
-      fixpoint_exprl
-  in
-  let (_, _, _, typel), _, ctx, _ =
-    ComFixpoint.interp_recursive ~check_recursivity:false ~cofix:false fixl
+let recompute_binder_list (rec_order, fixpoint_exprl) =
+  let _, _, ((_, _, _, typel), _, uctx, _) =
+    ComFixpoint.interp_recursive ~check_recursivity:false (false, CFixRecOrder rec_order) fixpoint_exprl
   in
   let constr_expr_typel =
     with_full_print
       (List.map (fun c ->
-           Constrextern.extern_constr (Global.env ()) (Evd.from_ctx ctx)
+           Constrextern.extern_constr (Global.env ()) (Evd.from_ctx uctx)
              (EConstr.of_constr c)))
       typel
   in
@@ -387,7 +377,7 @@ let generate_principle (evd : Evd.evar_map ref) pconstants on_error is_general
     end
   with e when CErrors.noncritical e -> on_error names e
 
-let register_struct is_rec fixpoint_exprl =
+let register_struct is_rec (rec_order, fixpoint_exprl) =
   let open EConstr in
   match fixpoint_exprl with
   | [{Vernacexpr.fname; univs; binders; rtype; body_def}] when not is_rec ->
@@ -416,7 +406,7 @@ let register_struct is_rec fixpoint_exprl =
     in
     (None, evd, List.rev rev_pconstants)
   | _ ->
-    let p = ComFixpoint.do_fixpoint ~poly:false fixpoint_exprl in
+    let p = ComFixpoint.do_mutually_recursive ~poly:false (CFixRecOrder rec_order, fixpoint_exprl) in
     assert (Option.is_empty p);
     let evd, rev_pconstants =
       List.fold_left
@@ -1748,20 +1738,18 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
     using_lemmas args ret_type body
 
 let do_generate_principle_aux pconstants on_error register_built
-    interactive_proof fixpoint_exprl : Declare.Proof.t option =
+    interactive_proof (rec_order, fixpoint_exprl as fix) : Declare.Proof.t option =
   List.iter
     (fun {Vernacexpr.notations} ->
       if not (List.is_empty notations) then
         CErrors.user_err (Pp.str "Function does not support notations for now"))
     fixpoint_exprl;
   let lemma, _is_struct =
-    match fixpoint_exprl with
-    | [ ( { Vernacexpr.rec_order =
-              Some {CAst.v = Constrexpr.CWfRec (wf_x, wf_rel)} } as
-        fixpoint_expr ) ] ->
+    match rec_order with
+    | [ Some { CAst.v = Constrexpr.CWfRec (wf_x, wf_rel) } ] ->
       let ( {Vernacexpr.fname; univs = _; binders; rtype; body_def} as
           fixpoint_expr ) =
-        match recompute_binder_list [fixpoint_expr] with
+        match recompute_binder_list fix with
         | [e] -> e
         | _ -> assert false
       in
@@ -1785,12 +1773,10 @@ let do_generate_principle_aux pconstants on_error register_built
             wf_x.CAst.v using_lemmas binders rtype body pre_hook
         , false )
       else (None, false)
-    | [ ( { Vernacexpr.rec_order =
-              Some {CAst.v = Constrexpr.CMeasureRec (wf_x, wf_mes, wf_rel_opt)}
-          } as fixpoint_expr ) ] ->
+    | [ Some { CAst.v = Constrexpr.CMeasureRec (wf_x, wf_mes, wf_rel_opt) } ] ->
       let ( {Vernacexpr.fname; univs = _; binders; rtype; body_def} as
           fixpoint_expr ) =
-        match recompute_binder_list [fixpoint_expr] with
+        match recompute_binder_list fix with
         | [e] -> e
         | _ -> assert false
       in
@@ -1818,16 +1804,14 @@ let do_generate_principle_aux pconstants on_error register_built
     | _ ->
       List.iter
         (function
-          | {Vernacexpr.rec_order} -> (
-            match rec_order with
-            | Some {CAst.v = Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _} ->
+            | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
               CErrors.user_err
                 (Pp.str
                    "Cannot use mutual definition with well-founded recursion \
                     or measure")
-            | _ -> () ))
-        fixpoint_exprl;
-      let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
+            | _ -> () )
+        rec_order;
+      let fixpoint_exprl = recompute_binder_list fix in
       let fix_names =
         List.map (function {Vernacexpr.fname} -> fname.CAst.v) fixpoint_exprl
       in
@@ -1835,7 +1819,7 @@ let do_generate_principle_aux pconstants on_error register_built
       let recdefs, _rec_impls = build_newrecursive fixpoint_exprl in
       let is_rec = List.exists (is_rec fix_names) recdefs in
       let lemma, evd, pconstants =
-        if register_built then register_struct is_rec fixpoint_exprl
+        if register_built then register_struct is_rec (rec_order, fixpoint_exprl)
         else (None, Evd.from_env (Global.env ()), pconstants)
       in
       let evd = ref evd in
@@ -2103,9 +2087,9 @@ let make_graph (f_ref : GlobRef.t) =
                      nal_tas)
               in
               let b' = add_args id.CAst.v new_args b in
+              Some (CAst.make (CStructRec (CAst.make rec_id))),
               { Vernacexpr.fname = id
               ; univs = None
-              ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id)))
               ; binders = nal_tas @ bl
               ; rtype = t
               ; body_def = Some b'
@@ -2115,15 +2099,15 @@ let make_graph (f_ref : GlobRef.t) =
         l
       | _ ->
         let fname = CAst.make (Label.to_id (Constant.label c)) in
-        [ { Vernacexpr.fname
+        [ None, { Vernacexpr.fname
           ; univs = None
-          ; rec_order = None
           ; binders = nal_tas
           ; rtype = t
           ; body_def = Some b
           ; notations = [] } ]
     in
     let mp = Constant.modpath c in
+    let expr_list = List.split expr_list in
     let pstate =
       do_generate_principle_aux [(c, UVars.Instance.empty)] error_error false
         false expr_list
@@ -2133,7 +2117,7 @@ let make_graph (f_ref : GlobRef.t) =
     List.iter
       (fun {Vernacexpr.fname = {CAst.v = id}} ->
         add_Function false (Constant.make2 mp (Label.of_id id)))
-      expr_list
+      (snd expr_list)
 
 (* *************** statically typed entrypoints ************************* *)
 
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
index 28751c4501bc..0050b0c6f7c4 100644
--- a/plugins/funind/gen_principle.mli
+++ b/plugins/funind/gen_principle.mli
@@ -12,9 +12,9 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle_interactive :
-  Vernacexpr.fixpoint_expr list -> Declare.Proof.t
+  Vernacexpr.fixpoints_expr -> Declare.Proof.t
 
-val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
+val do_generate_principle : Vernacexpr.fixpoints_expr -> unit
 val make_graph : Names.GlobRef.t -> unit
 
 (* Can be thrown by build_{,case}_scheme *)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index c37c31e44c64..41292b1e09b4 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -36,7 +36,7 @@ val pr_sort_expr : sort_expr -> Pp.t
 val pr_guard_annot
   :  (constr_expr -> Pp.t)
   -> local_binder_expr list
-  -> recursion_order_expr option
+  -> fixpoint_order_expr option
   -> Pp.t
 
 val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index d187bc8cbf6b..be942ffee8b9 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -11,7 +11,9 @@
 open Pp
 open Util
 open Names
+open Constrexpr
 open Constrintern
+open Vernacexpr
 
 (* 3c| Fixpoints and co-fixpoints *)
 
@@ -69,12 +71,12 @@ let non_full_mutual_message x xge y yge isfix rest =
     else
       Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in
   let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in
-  let k = if isfix then "fixpoint" else "cofixpoint" in
+  let k = Decls.(match isfix with Fixpoint -> "defined fixpoint" | CoFixpoint -> "defined cofixpoint" | _ -> "dependent definition") in
   let w =
-    if isfix
+    if isfix <> Decls.CoFixpoint
     then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
     else mt () in
-  strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++
+  strbrk "Not a fully mutually " ++ str k ++ fnl () ++
   str "(" ++ e ++ str ")." ++ fnl () ++ w
 
 let warn_non_full_mutual =
@@ -85,7 +87,7 @@ let warn_non_full_mutual =
 let warn_non_recursive =
   CWarnings.create ~name:"non-recursive" ~category:CWarnings.CoreCategories.fixpoints
          (fun (x,isfix) ->
-          let k = if isfix then "fixpoint" else "cofixpoint" in
+          let k = Decls.(match isfix with Fixpoint -> "fixpoint" | CoFixpoint -> "cofixpoint" | _ -> "definition") in
           strbrk "Not a truly recursive " ++ str k ++ str ".")
 
 let check_true_recursivity env evd ~isfix fixl =
@@ -103,32 +105,71 @@ let check_true_recursivity env evd ~isfix fixl =
     | [x,Inr []] -> warn_non_recursive (x,isfix)
     | _ -> ()
 
+let extract_decreasing_argument ~structonly { CAst.v = v; _ } =
+  let open Constrexpr in
+  match v with
+  | CStructRec na -> na
+  | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
+  | CMeasureRec (None,_,_) when not structonly ->
+    CErrors.user_err Pp.(str "Decreasing argument must be specified in measure clause.")
+  | _ ->
+    CErrors.user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.")
+
+(* This is a special case: if there's only one binder, we pick it as
+   the recursive argument if none is provided. *)
+let adjust_rec_order ~structonly binders rec_order =
+  let rec_order =
+      match binders, rec_order with
+      | [CLocalAssum([{ CAst.v = Name x }],_,_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+        CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+      | [CLocalDef({ CAst.v = Name x },_,_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+        CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+      | _, x -> x
+  in
+  extract_decreasing_argument ~structonly rec_order
+
 (* Interpret the index of a recursion order annotation *)
 exception Found of int
-let find_rec_annot bl ctx na =
-  let name = Name na.CAst.v in
-  try
-    Context.Rel.fold_outside (fun decl n ->
-      match Context.Rel.Declaration.(get_value decl, Name.equal (get_name decl) name) with
-      | None, true -> raise (Found n)
-      | Some _, true ->
-          let loc = List.find_map (fun id -> if Name.equal name id.CAst.v then Some id.CAst.loc else None) (Constrexpr_ops.names_of_local_binders bl) in
-          let loc = Option.default na.CAst.loc loc in
-          CErrors.user_err ?loc
-            (Name.print name ++ str" must be a proper parameter and not a local definition.")
-      | None, false -> n + 1
-      | Some _, false -> n (* let-ins don't count *))
-      ~init:0 ctx |> ignore;
-    CErrors.user_err ?loc:na.loc
-      (str "No parameter named " ++ Id.print na.v ++ str".");
-  with
-    Found k -> k
-
-let interp_fix_context ~program_mode ~cofix env sigma fix =
-  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma fix.Vernacexpr.binders in
-  if not cofix && Context.Rel.nhyps ctx = 0 then CErrors.user_err Pp.(str "A fixpoint needs at least one parameter.");
-  let annot = Option.map (find_rec_annot fix.Vernacexpr.binders ctx) fix.Vernacexpr.rec_order in
-  sigma, ((env', ctx), (impl_env, imps), annot)
+let find_rec_annot ~structonly Vernacexpr.{binders} (_, ctx) = function
+  | None ->
+    if Int.equal (Context.Rel.nhyps ctx) 0 then CErrors.user_err Pp.(str "A fixpoint needs at least one parameter.");
+    List.interval 0 (Context.Rel.nhyps ctx - 1)
+  | Some fix_order ->
+    let na = adjust_rec_order ~structonly binders fix_order in
+    let name = Name na.CAst.v in
+    try
+      Context.Rel.fold_outside (fun decl n ->
+        match Context.Rel.Declaration.(get_value decl, Name.equal (get_name decl) name) with
+        | None, true -> raise (Found n)
+        | Some _, true ->
+            let loc = List.find_map (fun id -> if Name.equal name id.CAst.v then Some id.CAst.loc else None) (Constrexpr_ops.names_of_local_binders binders) in
+            let loc = Option.default na.CAst.loc loc in
+            CErrors.user_err ?loc
+              (Name.print name ++ str" must be a proper parameter and not a local definition.")
+        | None, false -> n + 1
+        | Some _, false -> n (* let-ins don't count *))
+        ~init:0 ctx |> ignore;
+      CErrors.user_err ?loc:na.loc
+        (str "No parameter named " ++ Id.print na.v ++ str".");
+    with
+      Found k -> [k]
+
+let interp_rec_annot fixl ctxl (structonly, rec_order) =
+  let open Pretyping in
+  match rec_order with
+  (* If recursive argument was not given by user, we try all args.
+     An earlier approach was to look only for inductive arguments,
+     but doing it properly involves delta-reduction, and it finally
+     doesn't seem to worth the effort (except for huge mutual
+     fixpoints ?) *)
+  | CFixRecOrder fix_orders -> Decls.Fixpoint, {possibly_cofix = false; possible_fix_indices = List.map3 (find_rec_annot ~structonly) fixl ctxl fix_orders}
+  | CCoFixRecOrder -> Decls.CoFixpoint, {possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) fixl}
+  | CUnknownRecOrder -> Decls.Definition, {possibly_cofix = true; possible_fix_indices = List.map2 (fun fix ctx -> find_rec_annot ~structonly fix ctx None) fixl ctxl}
+(*  | CNoRecOrder -> (false, [])*)
+
+let interp_fix_context ~program_mode env sigma {Vernacexpr.binders} =
+  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma binders in
+  sigma, ((env', ctx), (impl_env, imps))
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
@@ -147,19 +188,6 @@ let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences (ctx,_,recindex) =
-  (* A recursive index is characterized by the number of lambdas to
-     skip before finding the relevant inductive argument *)
-  match recindex with
-  | Some i -> [i]
-  | None ->
-      (* If recursive argument was not given by user, we try all args.
-         An earlier approach was to look only for inductive arguments,
-         but doing it properly involves delta-reduction, and it finally
-         doesn't seem to worth the effort (except for huge mutual
-         fixpoints ?) *)
-      List.interval 0 (Context.Rel.nhyps ctx - 1)
-
 type ('constr, 'types, 'r) recursive_preentry =
   Id.t list * 'r list * 'constr option list * 'types list
 
@@ -170,16 +198,17 @@ let fix_proto sigma =
 let fix_proto_relevance = EConstr.ERelevance.relevant
 (* Would probably be overkill to use a specific fix_proto in SProp when in SProp?? *)
 
-let interp_recursive_evars env ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) =
+let interp_recursive_evars env ~program_mode rec_order fixl =
   let open Context.Named.Declaration in
   let open EConstr in
   let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in
 
   (* Interp arities allowing for unresolved types *)
   let sigma, decl = interp_mutual_univ_decl_opt env (List.map (fun Vernacexpr.{univs} -> univs) fixl) in
-  let sigma, (fixctxs, fiximppairs, fixannots) =
-    on_snd List.split3 @@
-      List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
+  let sigma, (fixctxs, fiximppairs) =
+    on_snd List.split @@
+      List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma) sigma fixl in
+  let fixkind, fixannot = interp_rec_annot fixl fixctxs rec_order in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
   let sigma, (fixccls,fixrs,fixcclimps) =
     on_snd List.split3 @@
@@ -226,7 +255,7 @@ let interp_recursive_evars env ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_ex
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,decl,sigma), (fixnames,fixrs,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+  (env,rec_sign,decl,sigma), (fixnames,fixrs,fixdefs,fixtypes), List.combine fixctxs fiximps, fixkind, fixannot
 
 let check_recursive ~isfix env evd (fixnames,_,fixdefs,_) =
   if List.for_all Option.has_some fixdefs then begin
@@ -242,33 +271,26 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
   Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
 
 (* XXX: Unify with interp_recursive  *)
-let interp_recursive ?(check_recursivity=true) ?typing_flags ~cofix l :
-  ( (Constr.t, Constr.types, Sorts.relevance) recursive_preentry *
+let interp_recursive ?(check_recursivity=true) ?typing_flags rec_order l :
+  Decls.definition_object_kind * Pretyping.possible_guard * ((Constr.t, Constr.types, Sorts.relevance) recursive_preentry *
     UState.universe_decl * UState.t *
-    (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
+    (EConstr.rel_context * Impargs.manual_implicits) list) =
   let env = Global.env () in
   let env = Environ.update_typing_flags ?typing_flags env in
-  let (env,_,pl,evd),fix,info = interp_recursive_evars env ~program_mode:false ~cofix l in
-  if check_recursivity then check_recursive ~isfix:(not cofix) env evd fix;
+  let (env,_,pl,evd),fix,info,isfix,possible_guards = interp_recursive_evars env ~program_mode:false rec_order l in
+  if check_recursivity then check_recursive ~isfix env evd fix;
   let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in
   let uctx,fix = ground_fixpoint env evd fix in
-  (fix,pl,uctx,info)
+  isfix, possible_guards, (fix,pl,uctx,info)
 
-let build_recthms ~indexes fixnames fixtypes fiximps =
-  let fix_kind, possible_guard = match indexes with
-    | Some possible_fix_indices -> Decls.Fixpoint, Pretyping.{possibly_cofix = false; possible_fix_indices}
-    | None -> Decls.CoFixpoint, Pretyping.{possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) fixtypes}
-  in
-  let thms =
-    List.map3 (fun name typ (ctx,impargs,_) ->
-        let args = List.map Context.Rel.Declaration.get_name ctx in
-        Declare.CInfo.make ~name ~typ ~args ~impargs ()
-      ) fixnames fixtypes fiximps
-  in
-  fix_kind, possible_guard, thms
+let build_recthms fixnames fixtypes fiximps =
+  List.map3 (fun name typ (ctx,impargs) ->
+      let args = List.map Context.Rel.Declaration.get_name ctx in
+      Declare.CInfo.make ~name ~typ ~args ~impargs ()
+    ) fixnames fixtypes fiximps
 
-let declare_recursive ?indexes ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
-  let fix_kind, possible_guard, cinfo = build_recthms ~indexes fixnames fixtypes fiximps in
+let declare_recursive ~fix_kind ~possible_guard ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+  let cinfo = build_recthms fixnames fixtypes fiximps in
   let kind = Decls.IsDefinition fix_kind in
   let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?typing_flags ?user_warns ~ntns () in
   match Option.List.map (fun x -> x) fixdefs with
@@ -286,41 +308,7 @@ let declare_recursive ?indexes ?scope ?clearbody ~poly ?typing_flags ?user_warns
       ~bodies:fixdefs ~possible_guard ?using evd in
     Some lemma
 
-let extract_decreasing_argument ~structonly { CAst.v = v; _ } =
-  let open Constrexpr in
-  match v with
-  | CStructRec na -> na
-  | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
-  | CMeasureRec (None,_,_) when not structonly ->
-    CErrors.user_err Pp.(str "Decreasing argument must be specified in measure clause.")
-  | _ ->
-    CErrors.user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.")
-
-(* This is a special case: if there's only one binder, we pick it as
-   the recursive argument if none is provided. *)
-let adjust_rec_order ~structonly binders rec_order =
-  let rec_order = Option.map (fun rec_order ->
-      let open Constrexpr in
-      match binders, rec_order with
-      | [CLocalAssum([{ CAst.v = Name x }],_,_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
-        CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
-      | [CLocalDef({ CAst.v = Name x },_,_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
-        CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
-      | _, x -> x) rec_order
-  in
-  Option.map (extract_decreasing_argument ~structonly) rec_order
-
-let do_fixpoint ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (fixl : Vernacexpr.fixpoint_expr list) : Declare.Proof.t option =
-  let fixl = List.map (fun fix ->
-      Vernacexpr.{ fix
-                   with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in
-  let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
-  let (_, _, _, info as fix) = interp_recursive ~cofix:false ?typing_flags fixl in
-  let possible_indexes = List.map compute_possible_guardness_evidences info in
-  declare_recursive ~indexes:possible_indexes ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix ntns
-
-let do_cofixpoint ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (fixl : Vernacexpr.cofixpoint_expr list) =
-  let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
+let do_mutually_recursive ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) : Declare.Proof.t option =
   let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
-  let cofix, ntns = interp_recursive ~cofix:true fixl, ntns in
-  declare_recursive ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using cofix ntns
+  let fix_kind, possible_guard, fix = interp_recursive ?typing_flags (true, rec_order) fixl in
+  declare_recursive ~fix_kind ~possible_guard ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix ntns
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 6e4101b968a5..58313b1ec9ca 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -15,38 +15,20 @@ open Vernacexpr
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
-val do_fixpoint
+val do_mutually_recursive
   : ?scope:Locality.definition_scope
   -> ?clearbody:bool
   -> poly:bool
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
   -> ?using:Vernacexpr.section_subset_expr
-  -> fixpoint_expr list
-  -> Declare.Proof.t option
-
-val do_cofixpoint
-  : ?scope:Locality.definition_scope
-  -> ?clearbody:bool
-  -> poly:bool
-  -> ?typing_flags:Declarations.typing_flags
-  -> ?user_warns:UserWarn.t
-  -> ?using:Vernacexpr.section_subset_expr
-  -> cofixpoint_expr list
+  -> recursives_expr
   -> Declare.Proof.t option
 
 (************************************************************************)
 (** Internal API  *)
 (************************************************************************)
 
-(** Typing global fixpoints and cofixpoint_expr *)
-
-val adjust_rec_order
-  :  structonly:bool
-  -> Constrexpr.local_binder_expr list
-  -> Constrexpr.recursion_order_expr option
-  -> lident option
-
 (** names / relevance / defs / types *)
 type ('constr, 'types, 'r) recursive_preentry = Id.t list * 'r list * 'constr option list * 'types list
 
@@ -54,27 +36,25 @@ type ('constr, 'types, 'r) recursive_preentry = Id.t list * 'r list * 'constr op
 val interp_recursive_evars :
   Environ.env ->
   (* Misc arguments *)
-  program_mode:bool -> cofix:bool ->
+  program_mode:bool ->
   (* Notations of the fixpoint / should that be folded in the previous argument? *)
-  lident option fix_expr_gen list ->
+  bool * recursion_order_expr ->
+  recursive_expr_gen list ->
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
   (EConstr.t, EConstr.types, EConstr.ERelevance.t) recursive_preentry *
   (* ctx per mutual def / implicits / struct annotations *)
-  (EConstr.rel_context * Impargs.manual_implicits * int option) list
+  (EConstr.rel_context * Impargs.manual_implicits) list * Decls.definition_object_kind * Pretyping.possible_guard
 
 (** Exported for Funind *)
 
 val interp_recursive
   :  ?check_recursivity:bool
   -> ?typing_flags:Declarations.typing_flags
-  -> cofix:bool
-  -> lident option fix_expr_gen list
-  -> (Constr.t, Constr.types, Sorts.relevance) recursive_preentry *
-     UState.universe_decl * UState.t *
-     (EConstr.rel_context * Impargs.manual_implicits * int option) list
-
-(** Very private function, do not use *)
-val compute_possible_guardness_evidences :
-  ('a, 'b, 'r) Context.Rel.pt * 'c * int option -> int list
+  -> bool * Vernacexpr.recursion_order_expr
+  -> recursive_expr_gen list
+  -> Decls.definition_object_kind * Pretyping.possible_guard *
+     ((Constr.t, Constr.types, Sorts.relevance) recursive_preentry *
+      UState.universe_decl * UState.t *
+      (EConstr.rel_context * Impargs.manual_implicits) list)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c1ccc477e4a4..975b07394752 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -213,12 +213,11 @@ let out_def = function
 let collect_evars_of_term evd c ty =
   Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty)
 
-let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using kind fixl =
-  let cofix = kind = Decls.CoFixpoint in
-  let (env, rec_sign, udecl, evd), fix, info =
+let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) =
+  let (env, rec_sign, udecl, evd), fix, info, kind, possible_guard =
     let env = Global.env () in
     let env = Environ.update_typing_flags ?typing_flags env in
-    interp_recursive_evars env ~cofix ~program_mode:true fixl
+    interp_recursive_evars env ~program_mode:true (false, rec_order) fixl
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instantiated *)
@@ -236,13 +235,10 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
         (List.length rec_sign) ~deps def typ in
     (def, evars, typ)
   in
-  let fiximps = List.map pi2 info in
+  let fiximps = List.map snd info in
   let fixdefs = List.map out_def fixdefs in
   let bodies, obls, typs = List.split3 (List.map4 collect_evars fixnames fixdefs fixtypes fiximps) in
   let cinfo = List.map3 (fun name typ impargs -> Declare.CInfo.make ~name ~typ ~impargs ()) fixnames typs fiximps in
-  let possible_guard =
-    if cofix then Pretyping.{possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) info}
-    else Pretyping.{possibly_cofix = false; possible_fix_indices = List.map ComFixpoint.compute_possible_guardness_evidences info} in
   let () =
     (* An early check of guardedness before working on the obligations *)
     let fixdecls =
@@ -258,9 +254,8 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
   let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns () in
   Declare.Obls.add_mutual_definitions ~pm ~info ~cinfo ~opaque:false ~uctx ~bodies ~possible_guard ?using obls
 
-let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
-  let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
-    match g, l with
+let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (fix_order, l) =
+  match fix_order, l with
     | [Some { CAst.v = CWfRec (n,r) }],
       [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
@@ -280,16 +275,17 @@ let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
         build_wellfounded pm (id, univs, binders, rtype, out_def body_def) ~scope ?clearbody poly ?typing_flags ?user_warns
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
-    | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
-      let annots = List.map (fun fix ->
-          Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
-      let kind = Decls.Fixpoint in
-      let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using kind l
+    | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) fix_order ->
+      do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CFixRecOrder fix_order, l)
     | _, _ ->
       CErrors.user_err
         (str "Well-founded fixpoints not allowed in mutually recursive blocks.")
 
 let do_cofixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fixl =
-  let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using Decls.CoFixpoint fixl
+  do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, fixl)
+
+let do_mutually_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, l) =
+  Vernacexpr.(match rec_order with
+  | CFixRecOrder fix_order -> do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (fix_order, l)
+  | CCoFixRecOrder -> do_cofixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l
+  | CUnknownRecOrder -> user_err Pp.(strbrk "Automatic detection of fix/cofix not implemented for Program."))
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index b6879ecdc6e3..408963a68487 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -19,7 +19,7 @@ val do_fixpoint :
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
   -> ?using:Vernacexpr.section_subset_expr
-  -> fixpoint_expr list
+  -> fixpoints_expr
   -> Declare.OblState.t
 
 val do_cofixpoint :
@@ -30,5 +30,16 @@ val do_cofixpoint :
   -> ?typing_flags:Declarations.typing_flags
   -> ?user_warns:UserWarn.t
   -> ?using:Vernacexpr.section_subset_expr
-  -> cofixpoint_expr list
+  -> cofixpoints_expr
+  -> Declare.OblState.t
+
+val do_mutually_recursive :
+     pm:Declare.OblState.t
+  -> scope:Locality.definition_scope
+  -> ?clearbody:bool
+  -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
+  -> ?user_warns:UserWarn.t
+  -> ?using:Vernacexpr.section_subset_expr
+  -> recursives_expr
   -> Declare.OblState.t
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 7fcf3abfb763..ae6fe8db8a1d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -270,9 +270,9 @@ GRAMMAR EXTEND Gram
       | f = inductive_token; indl = LIST1 inductive_or_record_definition SEP "with" ->
           { VernacInductive (f, indl) }
       | "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
-          { VernacFixpoint (NoDischarge, recs) }
+          { VernacFixpoint (NoDischarge, List.split recs) }
       | IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
-          { VernacFixpoint (DoDischarge, recs) }
+          { VernacFixpoint (DoDischarge, List.split recs) }
       | "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
           { VernacCoFixpoint (NoDischarge, corecs) }
       | IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
@@ -503,13 +503,13 @@ GRAMMAR EXTEND Gram
         rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations ->
           { let binders, rec_order = bl in
-            {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
+            ((rec_order : Constrexpr.fixpoint_order_expr option), {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations})
           } ] ]
   ;
   cofix_definition:
     [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
-        { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
+        { {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations}
         } ]]
   ;
   (* Rewrite Rules *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d4ab14f78101..89674e698c81 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -524,7 +524,7 @@ let pr_notation_declaration ntn_decl =
 let pr_where_notation decl_ntn =
   fnl () ++ keyword "where " ++ pr_notation_declaration decl_ntn
 
-let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
+let pr_rec_definition (rec_order, { fname; univs; binders; rtype; body_def; notations }) =
   let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
   let annot = pr_guard_annot pr_lconstr_expr binders rec_order in
   pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot
@@ -927,7 +927,7 @@ let pr_synpure_vernac_expr v =
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
     )
 
-  | VernacFixpoint (local, recs) ->
+  | VernacFixpoint (local, (rec_order, recs)) ->
     let local = match local with
       | DoDischarge -> "Let "
       | NoDischarge -> ""
@@ -935,7 +935,7 @@ let pr_synpure_vernac_expr v =
     return (
       hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
              prlist_with_sep (fun _ -> fnl () ++ keyword "with"
-                                       ++ spc ()) pr_rec_definition recs)
+                                       ++ spc ()) pr_rec_definition (List.combine rec_order recs))
     )
 
   | VernacCoFixpoint (local, corecs) ->
diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli
index a43900aeaf14..711234e4b234 100644
--- a/vernac/ppvernac.mli
+++ b/vernac/ppvernac.mli
@@ -16,7 +16,7 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
 val pr_syntax_modifier : Vernacexpr.syntax_modifier CAst.t -> Pp.t
 
 (** Prints a fixpoint body *)
-val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t
+val pr_rec_definition : Constrexpr.fixpoint_order_expr option * Vernacexpr.recursive_expr_gen -> Pp.t
 
 (** Prints a scheme *)
 val pr_onescheme : Names.lident option * Vernacexpr.scheme -> Pp.t
diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml
index 78e2244fc00b..2291a49359e1 100644
--- a/vernac/vernac_classifier.ml
+++ b/vernac/vernac_classifier.ml
@@ -118,7 +118,7 @@ let classify_vernac e =
       let ids = List.map (fun (({v=i}, _), _) -> i) l in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
       VtStartProof (guarantee,ids)
-    | VernacFixpoint (discharge,l) ->
+    | VernacFixpoint (discharge,(_,l)) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
          if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4721ecf10728..2e2c3f27806b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1086,22 +1086,22 @@ let vernac_fixpoint_common ~atts l =
   List.iter (fun { fname } -> check_name_freshness scope fname) l;
   scope
 
-let vernac_fixpoint ~atts ~pm l =
+let vernac_fixpoint ~atts ~pm (rec_order,fixl as fix) =
   let open DefAttributes in
-  let scope = vernac_fixpoint_common ~atts l in
+  let scope = vernac_fixpoint_common ~atts fixl in
   let poly, typing_flags, program_mode, clearbody, using, user_warns =
     atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in
   if program_mode then
     (* XXX: Switch to the attribute system and match on ~atts *)
-    let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
+    let opens = List.exists (fun { body_def } -> Option.is_empty body_def) fixl in
     if opens then
       CErrors.user_err Pp.(str"Program Fixpoint requires a body.")
     else
       let pm = Option.get pm in
-      let pm = ComProgramFixpoint.do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l in
+      let pm = ComProgramFixpoint.do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fix in
       Some pm, None
   else
-    let proof = ComFixpoint.do_fixpoint ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l in
+    let proof = ComFixpoint.do_mutually_recursive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl) in
     pm, proof
 
 let vernac_cofixpoint_common ~atts l =
@@ -1125,7 +1125,7 @@ let vernac_cofixpoint ~atts ~pm l =
       let pm = ComProgramFixpoint.do_cofixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l in
       Some pm, None
   else
-    let proof = ComFixpoint.do_cofixpoint ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l in
+    let proof = ComFixpoint.do_mutually_recursive ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, l) in
     pm, proof
 
 let vernac_scheme l =
@@ -2455,7 +2455,7 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with
     vtdefault(fun () -> vernac_inductive ~atts finite l)
 
   | VernacFixpoint (discharge, l) ->
-    let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
+    let opens = List.exists (fun { body_def } -> Option.is_empty body_def) (snd l) in
     let discharge = discharge, "\"Let Fixpoint\"", "\"#[local] Fixpoint\"" in
     (if opens then
       vtopenproof (fun () ->
diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli
index 6d5f5973500f..a9cc460ca521 100644
--- a/vernac/vernacexpr.mli
+++ b/vernac/vernacexpr.mli
@@ -172,18 +172,24 @@ type notation_declaration =
   ; ntn_decl_modifiers : syntax_modifier CAst.t list
   }
 
-type 'a fix_expr_gen =
+type recursion_order_expr =
+  | CFixRecOrder of fixpoint_order_expr option list
+  | CCoFixRecOrder
+  | CUnknownRecOrder
+
+type recursive_expr_gen =
   { fname : lident
   ; univs : universe_decl_expr option
-  ; rec_order : 'a
   ; binders : local_binder_expr list
   ; rtype : constr_expr
   ; body_def : constr_expr option
   ; notations : notation_declaration list
   }
 
-type fixpoint_expr = recursion_order_expr option fix_expr_gen
-type cofixpoint_expr = unit fix_expr_gen
+type fixpoint_expr = fixpoint_order_expr option * recursive_expr_gen
+type fixpoints_expr = fixpoint_order_expr option list * recursive_expr_gen list
+type cofixpoints_expr = recursive_expr_gen list
+type recursives_expr = recursion_order_expr * recursive_expr_gen list
 
 type local_decl_expr =
   | AssumExpr of lname * local_binder_expr list * constr_expr
@@ -412,8 +418,8 @@ type nonrec synpure_vernac_expr =
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
   | VernacSymbol of (ident_decl list * constr_expr) with_coercion list
   | VernacInductive of inductive_kind * (inductive_expr * notation_declaration list) list
-  | VernacFixpoint of discharge * fixpoint_expr list
-  | VernacCoFixpoint of discharge * cofixpoint_expr list
+  | VernacFixpoint of discharge * fixpoints_expr
+  | VernacCoFixpoint of discharge * cofixpoints_expr
   | VernacScheme of (lident option * scheme) list
   | VernacSchemeEquality of equality_scheme_type * Libnames.qualid Constrexpr.or_by_notation
   | VernacCombinedScheme of lident * lident list