[vernacexpr] Refactor fixpoint AST.

We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.

More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.

Feedback on the naming of the records fields is welcome.

This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.

cc: #6019

13 files changed, 121 insertions, 124 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 3f13d772ab..b7da4f964d 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -107,14 +107,15 @@ let check_mutuality env evd isfix fixl =
        warn_non_full_mutual (x,xge,y,yge,isfix,rest)
     | _ -> ()
 
-type structured_fixpoint_expr = {
-  fix_name : Id.t;
-  fix_univs : universe_decl_expr option;
-  fix_annot : lident option;
-  fix_binders : local_binder_expr list;
-  fix_body : constr_expr option;
-  fix_type : constr_expr
-}
+type structured_fixpoint_expr =
+  { fix_name : Id.t
+  ; fix_univs : Constrexpr.universe_decl_expr option
+  ; fix_annot : lident option
+  ; fix_binders : local_binder_expr list
+  ; fix_body : constr_expr option
+  ; fix_type : constr_expr
+  ; fix_notations : Vernacexpr.decl_notation list
+  }
 
 let interp_fix_context ~program_mode ~cofix env sigma fix =
   let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
@@ -167,7 +168,7 @@ type recursive_preentry =
 let fix_proto sigma =
   Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")
 
-let interp_recursive ~program_mode ~cofix fixl notations =
+let interp_recursive ~program_mode ~cofix fixl =
   let open Context.Named.Declaration in
   let open EConstr in
   let env = Global.env() in
@@ -222,6 +223,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let sigma, fixdefs =
     Metasyntax.with_syntax_protection (fun () ->
+      let notations = List.map_append (fun { fix_notations } -> fix_notations) fixl in
       List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
       List.fold_left4_map
         (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
@@ -248,8 +250,8 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
   let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
   Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
 
-let interp_fixpoint ~cofix l ntns =
-  let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in
+let interp_fixpoint ~cofix l =
+  let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
   check_recursive true env evd fix;
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
@@ -317,28 +319,25 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v
            "Well-founded induction requires Program Fixpoint or Function.")
 
 let extract_fixpoint_components ~structonly l =
-  let fixl, ntnl = List.split l in
-  let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
+  let open Vernacexpr in
+  List.map (fun { id_decl=({CAst.v=id},pl); rec_order; binders; rtype; body_def; notations } ->
       (* This is a special case: if there's only one binder, we pick it as the
-      recursive argument if none is provided. *)
-      let ann = Option.map (fun ann -> match bl, ann 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) ann
+         recursive argument if none is provided. *)
+      let rec_order = Option.map (fun 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) rec_order
       in
-      let ann = Option.map (extract_decreasing_argument ~structonly) ann in
-      {fix_name = id; fix_annot = ann; fix_univs = pl;
-       fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
-  fixl, List.flatten ntnl
+      let rec_order = Option.map (extract_decreasing_argument ~structonly) rec_order in
+      { fix_name = id; fix_annot = rec_order; fix_univs = pl;
+        fix_binders = binders; fix_body = body_def; fix_type = rtype; fix_notations = notations }) l
 
 let extract_cofixpoint_components l =
-  let fixl, ntnl = List.split l in
-  List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
-            {fix_name = id; fix_annot = None; fix_univs = pl;
-             fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
-  List.flatten ntnl
+  List.map (fun { Vernacexpr.id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations} ->
+      {fix_name = id; fix_annot = None; fix_univs = pl;
+       fix_binders = binders; fix_body = body_def; fix_type = rtype; fix_notations = notations}) l
 
 let check_safe () =
   let open Declarations in
@@ -346,8 +345,9 @@ let check_safe () =
   flags.check_universes && flags.check_guarded
 
 let do_fixpoint_common l =
-  let fixl, ntns = extract_fixpoint_components ~structonly:true l in
-  let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
+  let fixl = extract_fixpoint_components ~structonly:true l in
+  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
+  let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
 let do_fixpoint_interactive ~scope ~poly l : Lemmas.t =
@@ -362,16 +362,17 @@ let do_fixpoint ~scope ~poly l =
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
 let do_cofixpoint_common l =
-  let fixl,ntns = extract_cofixpoint_components l in
-  ntns, interp_fixpoint ~cofix:true fixl ntns
+  let fixl = extract_cofixpoint_components l in
+  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
+  interp_fixpoint ~cofix:true fixl, ntns
 
 let do_cofixpoint_interactive ~scope ~poly l =
-  let ntns, cofix = do_cofixpoint_common l in
+  let cofix, ntns = do_cofixpoint_common l in
   let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   lemma
 
 let do_cofixpoint ~scope ~poly l =
-  let ntns, cofix = do_cofixpoint_common l in
+  let cofix, ntns = do_cofixpoint_common l in
   declare_fixpoint_generic ~scope ~poly cofix ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 982d316605..1018c463c6 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -18,29 +18,30 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
 
 val do_fixpoint :
-  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
 
 val do_cofixpoint :
-  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)
 (************************************************************************)
 
-type structured_fixpoint_expr = {
-  fix_name : Id.t;
-  fix_univs : Constrexpr.universe_decl_expr option;
-  fix_annot : lident option;
-  fix_binders : local_binder_expr list;
-  fix_body : constr_expr option;
-  fix_type : constr_expr
-}
+type structured_fixpoint_expr =
+  { fix_name : Id.t
+  ; fix_univs : Constrexpr.universe_decl_expr option
+  ; fix_annot : lident option
+  ; fix_binders : local_binder_expr list
+  ; fix_body : constr_expr option
+  ; fix_type : constr_expr
+  ; fix_notations : decl_notation list
+  }
 
 (** Typing global fixpoints and cofixpoint_expr *)
 
@@ -49,8 +50,7 @@ val interp_recursive :
   (* Misc arguments *)
   program_mode:bool -> cofix:bool ->
   (* Notations of the fixpoint / should that be folded in the previous argument? *)
-  structured_fixpoint_expr list -> decl_notation list ->
-
+  structured_fixpoint_expr list ->
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
@@ -63,22 +63,19 @@ val interp_recursive :
 (** Extracting the semantical components out of the raw syntax of
    (co)fixpoints declarations *)
 
-val extract_fixpoint_components : structonly:bool ->
-  (fixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation list
+val extract_fixpoint_components
+  : structonly:bool -> fixpoint_expr list -> structured_fixpoint_expr list
 
-val extract_cofixpoint_components :
-  (cofixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation list
+val extract_cofixpoint_components
+  : cofixpoint_expr list -> structured_fixpoint_expr list
 
-type recursive_preentry =
-  Id.t list * Sorts.relevance list * constr option list * types list
+type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
 
-val interp_fixpoint :
-  cofix:bool ->
-  structured_fixpoint_expr list -> decl_notation list ->
-  recursive_preentry * UState.universe_decl * UState.t *
-  (EConstr.rel_context * Impargs.manual_implicits * int option) list
+val interp_fixpoint
+  :  cofix:bool
+  -> structured_fixpoint_expr list
+  -> 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 :
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0fd65ad9b4..0104c99e41 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -244,10 +244,10 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~scope ~poly fixkind fixl ntns =
+let do_program_recursive ~scope ~poly fixkind fixl =
   let cofix = fixkind = DeclareObl.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info =
-    interp_recursive ~cofix ~program_mode:true fixl ntns
+    interp_recursive ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instantiated *)
@@ -289,16 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns =
   | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
   | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
+  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
   Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
 
 let do_program_fixpoint ~scope ~poly l =
-  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+  let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
-    | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+    | [Some { CAst.v = CWfRec (n,r) }],
+      [ Vernacexpr.{id_decl=({CAst.v=id},pl);binders;rtype;body_def;notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn
+        build_wellfounded (id, pl, binders, rtype, out_def body_def) poly r recarg notations
 
-    | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+    | [Some { CAst.v = CMeasureRec (n, m, r) }],
+      [Vernacexpr.{id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations }] ->
       (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *)
       let r = match n, r with
         | Some id, None ->
@@ -308,25 +311,18 @@ let do_program_fixpoint ~scope ~poly l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded (id, pl, bl, typ, out_def def) poly
-          (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
+        build_wellfounded (id, pl, binders, rtype, out_def body_def) poly
+          (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 fixl,ntns = extract_fixpoint_components ~structonly:true l in
-        let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
-          do_program_recursive ~scope ~poly fixkind fixl ntns
+      let fixl = extract_fixpoint_components ~structonly:true l in
+      let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
+      do_program_recursive ~scope ~poly fixkind fixl
 
     | _, _ ->
         user_err ~hdr:"do_program_fixpoint"
           (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let extract_cofixpoint_components l =
-  let fixl, ntnl = List.split l in
-  List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
-            {fix_name = id; fix_annot = None; fix_univs = pl;
-             fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
-  List.flatten ntnl
-
 let check_safe () =
   let open Declarations in
   let flags = Environ.typing_flags (Global.env ()) in
@@ -337,6 +333,6 @@ let do_fixpoint ~scope ~poly l =
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
 let do_cofixpoint ~scope ~poly l =
-  let fixl,ntns = extract_cofixpoint_components l in
-  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns;
+  let fixl = extract_cofixpoint_components l in
+  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index f25abb95c3..fa3d2b7020 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -4,8 +4,8 @@ open Vernacexpr
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 0c45ff11d7..c5cbb095ca 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -29,9 +29,6 @@ type obligation =
 
 type obligations = obligation array * int
 
-type notations =
-  (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
-
 type fixpoint_kind =
   | IsFixpoint of lident option list
   | IsCoFixpoint
@@ -46,7 +43,7 @@ type program_info =
   ; prg_deps : Id.t list
   ; prg_fixkind : fixpoint_kind option
   ; prg_implicits : Impargs.manual_implicits
-  ; prg_notations : notations
+  ; prg_notations : Vernacexpr.decl_notation list
   ; prg_poly : bool
   ; prg_scope : DeclareDef.locality
   ; prg_kind : Decls.definition_object_kind
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index a8dd5040cb..2a8fa734b3 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -24,9 +24,6 @@ type obligation =
 
 type obligations = obligation array * int
 
-type notations =
-  (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
-
 type fixpoint_kind =
   | IsFixpoint of lident option list
   | IsCoFixpoint
@@ -41,7 +38,7 @@ type program_info =
   ; prg_deps : Id.t list
   ; prg_fixkind : fixpoint_kind option
   ; prg_implicits : Impargs.manual_implicits
-  ; prg_notations : notations
+  ; prg_notations : Vernacexpr.decl_notation list
   ; prg_poly : bool
   ; prg_scope : DeclareDef.locality
   ; prg_kind : Decls.definition_object_kind
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 2b475f1ef9..678d4436d2 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -402,16 +402,18 @@ GRAMMAR EXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = ident_decl;
+    [ [ id_decl = ident_decl;
 	bl = binders_fixannot;
-        ty = type_cstr;
-	def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation ->
-	  { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ]
+        rtype = type_cstr;
+        body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation ->
+          { let binders, rec_order = bl in
+            {id_decl; rec_order; binders; rtype; body_def; notations}
+          } ] ]
   ;
   corec_definition:
-    [ [ id = ident_decl; bl = binders; ty = type_cstr;
-        def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation ->
-          { ((id,bl,ty,def),ntn) } ] ]
+    [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
+        body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation ->
+          { {id_decl; rec_order=(); binders; rtype; body_def; notations} } ] ]
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> { c }
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index f97bc784c3..e5facd5fb6 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -69,7 +69,7 @@ val add_mutual_definitions
   -> ?kind:Decls.definition_object_kind
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t -> ?opaque:bool
-  -> DeclareObl.notations
+  -> Vernacexpr.decl_notation list
   -> DeclareObl.fixpoint_kind -> unit
 
 val obligation
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e676fe94db..835f5e0b75 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -419,15 +419,15 @@ let string_of_theorem_kind = let open Decls in function
     | l -> spc() ++
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-  let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) =
+  let pr_rec_definition { id_decl; rec_order; binders; rtype; body_def; notations } =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
-    let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in
-    pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot
-    ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_
-    ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def
-    ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
+    let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in
+    pr_ident_decl id_decl ++ pr_binders_arg binders ++ annot
+    ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype
+    ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def
+    ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations
 
   let pr_statement head (idpl,(bl,c)) =
     let env = Global.env () in
@@ -858,11 +858,11 @@ let string_of_definition_object_kind = let open Decls in function
           | DoDischarge -> keyword "Let" ++ spc ()
           | NoDischarge -> str ""
         in
-        let pr_onecorec ((iddecl,bl,c,def),ntn) =
-          pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++
-            spc() ++ pr_lconstr_expr env sigma c ++
-            pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++
-            prlist (pr_decl_notation @@ pr_constr env sigma) ntn
+        let pr_onecorec {id_decl; binders; rtype; body_def; notations } =
+          pr_ident_decl id_decl ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
+            spc() ++ pr_lconstr_expr env sigma rtype ++
+            pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++
+            prlist (pr_decl_notation @@ pr_constr env sigma) notations
         in
         return (
           hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli
index d4d49a09a3..9ade5afb87 100644
--- a/vernac/ppvernac.mli
+++ b/vernac/ppvernac.mli
@@ -14,7 +14,7 @@
 val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
 
 (** Prints a fixpoint body *)
-val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
+val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t
 
 (** Prints a vernac expression without dot *)
 val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index c9eb979a90..3bd252ecef 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -23,7 +23,7 @@ module Vernac_ :
     val command : vernac_expr Entry.t
     val syntax : vernac_expr Entry.t
     val vernac_control : vernac_control Entry.t
-    val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
+    val rec_definition : fixpoint_expr Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
     val main_entry : vernac_control option Entry.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 46ddf214ab..0205a653c5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -772,7 +772,7 @@ let vernac_inductive ~atts cum lo finite indl =
 
 let vernac_fixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
-    List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l;
   enforce_locality_exp atts.DefAttributes.locality discharge
 
 let vernac_fixpoint_interactive ~atts discharge l =
@@ -793,7 +793,7 @@ let vernac_fixpoint ~atts discharge l =
 
 let vernac_cofixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
-    List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l;
   enforce_locality_exp atts.DefAttributes.locality discharge
 
 let vernac_cofixpoint_interactive ~atts discharge l =
@@ -2358,7 +2358,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacInductive (cum, priv, finite, l) ->
     VtDefault(fun () -> vernac_inductive ~atts cum priv finite l)
   | VernacFixpoint (discharge, l) ->
-    let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in
+    let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
     if opens then
       VtOpenProof (fun () ->
         with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
@@ -2366,7 +2366,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
       VtDefault (fun () ->
         with_def_attributes ~atts vernac_fixpoint discharge l)
   | VernacCoFixpoint (discharge, l) ->
-    let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in
+    let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
     if opens then
       VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l)
     else
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ee1f839b8d..8b8123bd30 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -128,18 +128,25 @@ type definition_expr =
   | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
-type fixpoint_expr =
-    ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option
+type decl_notation = lstring * constr_expr * scope_name option
+
+type 'a fix_expr_gen =
+  { id_decl : ident_decl
+  ; rec_order : 'a
+  ; binders : local_binder_expr list
+  ; rtype : constr_expr
+  ; body_def : constr_expr option
+  ; notations : decl_notation list
+  }
 
-type cofixpoint_expr =
-    ident_decl * local_binder_expr list * constr_expr * constr_expr option
+type fixpoint_expr = recursion_order_expr option fix_expr_gen
+type cofixpoint_expr = unit fix_expr_gen
 
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
 type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
-type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
@@ -283,8 +290,8 @@ type nonrec vernac_expr =
   | VernacAssumption of (discharge * Decls.assumption_object_kind) *
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
   | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list
+  | VernacFixpoint of discharge * fixpoint_expr list
+  | VernacCoFixpoint of discharge * cofixpoint_expr list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list