Merge PR #10537: [vernacexpr] Refactor fixpoint AST.

Reviewed-by: SkySkimmer
Reviewed-by: gares

17 files changed, 306 insertions, 320 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 5f859b3e4b..1b75d3d966 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -148,9 +148,7 @@ END
 module Vernac = Pvernac.Vernac_
 module Tactic = Pltac
 
-type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
-
-let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
+let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
   Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
@@ -175,10 +173,10 @@ let () =
 
 let is_proof_termination_interactively_checked recsl =
   List.exists (function
-  | _,((_,( Some { CAst.v = CMeasureRec _ }
-          | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
-  | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
-  | _,((_,None,_,_,_),_) -> false) recsl
+  | _,( 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
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6e19ef4804..1987677d7d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open CErrors
 open Sorts
 open Util
@@ -157,17 +167,16 @@ let interp_casted_constr_with_implicits env sigma impls c  =
    and not as a constr
 *)
 
-let build_newrecursive
-    lnameargsardef  =
+let build_newrecursive lnameargsardef =
   let env0 = Global.env() in
   let sigma = Evd.from_env env0 in
   let (rec_sign,rec_impls) =
     List.fold_left
-      (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) ->
-        let arityc = Constrexpr_ops.mkCProdN bl arityc in
+      (fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } ->
+        let arityc = Constrexpr_ops.mkCProdN binders rtype in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
         let evd = Evd.from_env env0 in
-        let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in
+        let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in
         let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
         let open Context.Named.Declaration in
         let r = Sorts.Relevant in (* TODO relevance *)
@@ -175,26 +184,18 @@ let build_newrecursive
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
-    let f (_,bl,_,def) =
-      let def = abstract_glob_constr def bl in
-      interp_casted_constr_with_implicits
-        rec_sign sigma rec_impls def
+    let f { Vernacexpr.binders; body_def } =
+      match body_def with
+      | Some body_def ->
+        let def = abstract_glob_constr body_def binders in
+        interp_casted_constr_with_implicits
+          rec_sign sigma rec_impls def
+      | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
     in
     States.with_state_protection (List.map f) lnameargsardef
   in
   recdef,rec_impls
 
-let build_newrecursive l =
-  let l' = List.map
-    (fun ((fixna,_,bll,ar,body_opt),lnot) ->
-       match body_opt with
-         | Some body ->
-             (fixna,bll,ar,body)
-         | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
-    ) l
-  in
-  build_newrecursive l'
-
 let error msg = user_err Pp.(str msg)
 
 (* Checks whether or not the mutual bloc is recursive *)
@@ -237,8 +238,8 @@ let rec local_binders_length = function
   | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
   | Constrexpr.CLocalPattern _::bl -> assert false
 
-let prepare_body ((name,_,args,types,_),_) rt =
-  let n = local_binders_length args in
+let prepare_body { Vernacexpr.binders; rtype } rt =
+  let n = local_binders_length binders in
 (*   Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *)
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
@@ -336,13 +337,13 @@ let error_error names e =
     | _ -> raise e
 
 let generate_principle (evd:Evd.evar_map ref) pconstants on_error
-    is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
+    is_general do_built (fix_rec_l : Vernacexpr.fixpoint_expr list) recdefs interactive_proof
     (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
       Tacmach.tactic) : unit =
-  let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in
+  let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
-  let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
+  let funs_types =  List.map (function { Vernacexpr.rtype } -> rtype) fix_rec_l in
   try
     (* We then register the Inductive graphs of the functions  *)
     Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs;
@@ -359,7 +360,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
                  locate_ind
                  f_R_mut)
         in
-        let fname_kn (((fname,_),_,_,_,_),_) =
+        let fname_kn { Vernacexpr.fname } =
    let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
           locate_with_msg
             (pr_qualid f_ref++str ": Not an inductive type!")
@@ -398,23 +399,25 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
   with e when CErrors.noncritical e ->
     on_error names e
 
-let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
+let register_struct is_rec (fixpoint_exprl:  Vernacexpr.fixpoint_expr list) =
   match fixpoint_exprl with
-    | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
-      let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
+    | [ { Vernacexpr.fname; univs; binders; rtype; body_def } ] when not is_rec ->
+      let body = match body_def with
+        | Some body -> body
+        | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
       ComDefinition.do_definition
         ~program_mode:false
-        ~name:fname
+        ~name:fname.CAst.v
         ~poly:false
         ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-        ~kind:Decls.Definition pl
-        bl None body (Some ret_type);
+        ~kind:Decls.Definition univs
+        binders None body (Some rtype);
        let evd,rev_pconstants =
          List.fold_left
-           (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
+           (fun (evd,l) { Vernacexpr.fname } ->
             let evd,c =
               Evd.fresh_global
-                (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
+                (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in
             let (cst, u) = destConst evd c in
             let u = EInstance.kind evd u in
             evd,((cst, u) :: l)
@@ -427,10 +430,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
-           (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
+           (fun (evd,l) { Vernacexpr.fname } ->
             let evd,c =
               Evd.fresh_global
-                (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
+                (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in
             let (cst, u) = destConst evd c in
             let u = EInstance.kind evd u in
             evd,((cst, u) :: l)
@@ -464,7 +467,7 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf
   let unbounded_eq =
     let f_app_args =
       CAst.make @@ Constrexpr.CAppExpl(
-         (None,qualid_of_ident fname,None) ,
+         (None,qualid_of_ident fname.CAst.v,None) ,
          (List.map
             (function
                | {CAst.v=Anonymous} -> assert false
@@ -485,13 +488,13 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf
         (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
            functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
         );
-      derive_inversion [fname]
+      derive_inversion [fname.CAst.v]
     with e when CErrors.noncritical e ->
       (* No proof done *)
       ()
   in
   Recdef.recursive_definition ~interactive_proof
-    ~is_mes fname rec_impls
+    ~is_mes fname.CAst.v rec_impls
     type_of_f
     wf_rel_expr
     rec_arg_num
@@ -607,88 +610,93 @@ 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 : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
-  let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in
-  let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
+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_fixpoint ~cofix:false fixl in
   let constr_expr_typel =
     with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
   let fixpoint_exprl_with_new_bl =
-    List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ ->
-
-      let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in
-      (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
-    )
-      fixpoint_exprl constr_expr_typel
+    List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ ->
+      let binders, rtype = rebuild_bl [] binders fix_typ in
+      { fp with Vernacexpr.binders; rtype }
+    ) fixpoint_exprl constr_expr_typel
   in
   fixpoint_exprl_with_new_bl
 
 
 let do_generate_principle_aux pconstants on_error register_built interactive_proof
-    (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option =
-  List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
+    (fixpoint_exprl : Vernacexpr.fixpoint_expr list) : Lemmas.t option =
+  List.iter (fun { Vernacexpr.notations } ->
+      if not (List.is_empty notations)
+      then error "Function does not support notations for now") fixpoint_exprl;
   let lemma, _is_struct =
     match fixpoint_exprl with
-      | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] ->
-          let (((({CAst.v=name},pl),_,args,types,body)),_)  as fixpoint_expr =
-            match recompute_binder_list [fixpoint_expr] with
-              | [e] -> e
-              | _ -> assert false
-          in
-          let fixpoint_exprl = [fixpoint_expr] in
-          let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
-          let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
-          let using_lemmas = [] in
-          let pre_hook pconstants =
-            generate_principle
-              (ref (Evd.from_env (Global.env ())))
-              pconstants
-              on_error
-              true
-              register_built
-              fixpoint_exprl
-              recdefs
-              true
-          in
-          if register_built
-          then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
-          else None, false
-      |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] ->
-          let (((({CAst.v=name},_),_,args,types,body)),_)  as fixpoint_expr =
-            match recompute_binder_list [fixpoint_expr] with
-              | [e] -> e
-              | _ -> assert false
-          in
-          let fixpoint_exprl = [fixpoint_expr] in
-          let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
-          let using_lemmas = [] in
-          let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
-          let pre_hook pconstants =
-            generate_principle
-              (ref (Evd.from_env (Global.env ())))
-              pconstants
-              on_error
-              true
-              register_built
-              fixpoint_exprl
-              recdefs
-              true
-          in
-          if register_built
-          then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
-          else None, true
+      | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] ->
+        let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr =
+          match recompute_binder_list [fixpoint_expr] with
+          | [e] -> e
+          | _ -> assert false
+        in
+        let fixpoint_exprl = [fixpoint_expr] in
+        let body = match body_def with
+          | Some body -> body
+          | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
+        let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
+        let using_lemmas = [] in
+        let pre_hook pconstants =
+          generate_principle
+            (ref (Evd.from_env (Global.env ())))
+            pconstants
+            on_error
+            true
+            register_built
+            fixpoint_exprl
+            recdefs
+            true
+        in
+        if register_built
+        then register_wf interactive_proof fname rec_impls wf_rel 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] ->
+        let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr =
+          match recompute_binder_list [fixpoint_expr] with
+          | [e] -> e
+          | _ -> assert false
+        in
+        let fixpoint_exprl = [fixpoint_expr] in
+        let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
+        let using_lemmas = [] in
+        let body = match body_def with
+          | Some body -> body
+          | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
+        let pre_hook pconstants =
+          generate_principle
+            (ref (Evd.from_env (Global.env ())))
+            pconstants
+            on_error
+            true
+            register_built
+            fixpoint_exprl
+            recdefs
+            true
+        in
+        if register_built
+        then register_mes interactive_proof fname rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas binders rtype body pre_hook, true
+        else None, true
       | _ ->
-          List.iter (function ((_na,ord,_args,_body,_type),_not) ->
-                       match ord with
-                         | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
-                             error
-                               ("Cannot use mutual definition with well-founded recursion or measure")
-                         | _ -> ()
+        List.iter (function { Vernacexpr.rec_order } ->
+          match rec_order with
+          | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
+            error
+              ("Cannot use mutual definition with well-founded recursion or measure")
+          | _ -> ()
                     )
             fixpoint_exprl;
         let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
-        let fix_names =
-          List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl
-        in
+        let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in
         (* ok all the expressions are structural *)
         let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
         let is_rec = List.exists (is_rec fix_names) recdefs in
@@ -845,59 +853,59 @@ let make_graph (f_ref : GlobRef.t) =
      | None -> error "Cannot build a graph over an axiom!"
      | Some (body, _, _) ->
        let env = Global.env () in
-         let extern_body,extern_type =
-           with_full_print (fun () ->
-                (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
-                 Constrextern.extern_type false env sigma
-                   (EConstr.of_constr (*FIXME*) c_body.const_type)
-                )
+       let extern_body,extern_type =
+         with_full_print (fun () ->
+             (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
+              Constrextern.extern_type false env sigma
+                (EConstr.of_constr (*FIXME*) c_body.const_type)
              )
-             ()
-         in
-  let (nal_tas,b,t)  = get_args extern_body extern_type in
-  let expr_list =
-    match b.CAst.v with
-    | Constrexpr.CFix(l_id,fixexprl) ->
-      let l =
-        List.map
-          (fun (id,recexp,bl,t,b) ->
-             let { CAst.loc; v=rec_id } = match Option.get recexp with
-               | { CAst.v = CStructRec id } -> id
-               | { CAst.v = CWfRec (id,_) } -> id
-               | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid
-             in
-             let new_args =
-               List.flatten
-                 (List.map
-                    (function
-                      | Constrexpr.CLocalDef (na,_,_)-> []
-                      | Constrexpr.CLocalAssum (nal,_,_) ->
-                        List.map
-                          (fun {CAst.loc;v=n} -> CAst.make ?loc @@
-                            CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
-                          nal
-                      | Constrexpr.CLocalPattern _ -> assert false
-                    )
-                    nal_tas
-                 )
-             in
-             let b' = add_args id.CAst.v new_args b in
-             ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
-          )
-                      fixexprl
+           ) ()
+       in
+       let (nal_tas,b,t)  = get_args extern_body extern_type in
+       let expr_list =
+         match b.CAst.v with
+         | Constrexpr.CFix(l_id,fixexprl) ->
+           let l =
+             List.map
+               (fun (id,recexp,bl,t,b) ->
+                  let { CAst.loc; v=rec_id } = match Option.get recexp with
+                    | { CAst.v = CStructRec id } -> id
+                    | { CAst.v = CWfRec (id,_) } -> id
+                    | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid
+                  in
+                  let new_args =
+                    List.flatten
+                      (List.map
+                         (function
+                           | Constrexpr.CLocalDef (na,_,_)-> []
+                           | Constrexpr.CLocalAssum (nal,_,_) ->
+                             List.map
+                               (fun {CAst.loc;v=n} -> CAst.make ?loc @@
+                                 CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
+                               nal
+                           | Constrexpr.CLocalPattern _ -> assert false
+                         )
+                         nal_tas
+                      )
                   in
-                  l
-             | _ ->
-                let id = Label.to_id (Constant.label c) in
-                 [((CAst.make id,None),None,nal_tas,t,Some b),[]]
-         in
-         let mp = Constant.modpath c in
-         let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error  false false expr_list in
-         assert (Option.is_empty pstate);
-         (* We register the infos *)
-         List.iter
-           (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
-           expr_list)
+                  let b' = add_args id.CAst.v new_args b in
+                  { 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'; notations = []}
+               ) fixexprl in
+           l
+         | _ ->
+           let fname = CAst.make (Label.to_id (Constant.label c)) in
+           [{ 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 pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error  false false expr_list in
+       assert (Option.is_empty pstate);
+       (* We register the infos *)
+       List.iter
+         (fun { Vernacexpr.fname= {CAst.v=id} } ->
+            add_Function false (Constant.make2 mp (Label.of_id id)))
+         expr_list)
 
 (* *************** statically typed entrypoints ************************* *)
 
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 3bc52272ac..bfc9686ae5 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -5,12 +5,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 :
-  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit
+val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
 
-val do_generate_principle_interactive :
-  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Lemmas.t
+val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t
 
 val functional_induction :
   bool ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aaba36287a..8750a64ccc 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -106,8 +106,8 @@ let classify_vernac e =
          else GuaranteesOpacity
        in
         let ids, open_proof =
-          List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
-            id::l, b || p = None) ([],false) l in
+          List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} ->
+            id::l, b || body_def = None) ([],false) l in
         if open_proof
         then VtStartProof (guarantee,ids)
         else VtSideff (ids, VtLater)
@@ -118,8 +118,8 @@ let classify_vernac e =
          else GuaranteesOpacity
        in
         let ids, open_proof =
-          List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
-            id::l, b || p = None) ([],false) l in
+          List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } ->
+            id::l, b || body_def = None) ([],false) l in
         if open_proof
         then VtStartProof (guarantee,ids)
         else VtSideff (ids, VtLater)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 3f13d772ab..74c9bc2886 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -107,26 +107,20 @@ 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
-}
-
 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
+  let before, after =
+    if not cofix
+    then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order
+    else [], fix.Vernacexpr.binders in
   let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
   let sigma, (impl_env', ((env'', ctx'), imps')) =
     interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
   in
-  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
+  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
-  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in
+  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in
   let r = Retyping.relevance_of_type env sigma c in
   sigma, (c, r, impl)
 
@@ -135,7 +129,7 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
   Option.cata (fun body ->
     let env = push_rel_context ctx env_rec in
     let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in
-    sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body
+    sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def
 
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
@@ -167,16 +161,16 @@ 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 : 'a Vernacexpr.fix_expr_gen list) =
   let open Context.Named.Declaration in
   let open EConstr in
   let env = Global.env() in
-  let fixnames = List.map (fun fix -> fix.fix_name) fixl in
+  let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in
 
   (* Interp arities allowing for unresolved types *)
   let all_universes =
     List.fold_right (fun sfe acc ->
-        match sfe.fix_univs , acc with
+        match sfe.Vernacexpr.univs , acc with
         | None , acc -> acc
         | x , None -> x
         | Some ls , Some us ->
@@ -222,6 +216,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 { Vernacexpr.notations } -> 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 +243,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)
@@ -316,38 +311,29 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v
   | _ -> user_err Pp.(str
            "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) ->
-      (* 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
-      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 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
+(* 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 -> 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 check_safe () =
   let open Declarations in
   let flags = Environ.typing_flags (Global.env ()) in
   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 do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
+  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 } -> 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 =
@@ -361,17 +347,18 @@ let do_fixpoint ~scope ~poly l =
   declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns;
   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 do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
+  let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
+  let ntns = List.map_append (fun { Vernacexpr.notations } -> 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..4f8e9018de 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Constrexpr
 open Vernacexpr
 
 (** {6 Fixpoints and cofixpoints} *)
@@ -18,39 +17,35 @@ 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
-}
-
 (** Typing global fixpoints and cofixpoint_expr *)
 
+val adjust_rec_order
+  :  structonly:bool
+  -> Constrexpr.local_binder_expr list
+  -> Constrexpr.recursion_order_expr option
+  -> lident option
+
 (** Exported for Program *)
 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 ->
-
+  lident option fix_expr_gen list ->
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
@@ -60,25 +55,13 @@ val interp_recursive :
 
 (** Exported for Funind *)
 
-(** 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
+type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
 
-val extract_cofixpoint_components :
-  (cofixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation 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
+  -> lident option fix_expr_gen 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..c6e68effd7 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 { Vernacexpr.notations } -> 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.{fname={CAst.v=id}; univs; 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, univs, 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.{fname={CAst.v=id}; univs; 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,20 @@ 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, univs, 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 annots = List.map (fun fix ->
+          Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
+      let fixkind = DeclareObl.IsFixpoint annots in
+      let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
+      do_program_recursive ~scope ~poly fixkind l
 
     | _, _ ->
         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
@@ -336,7 +334,7 @@ let do_fixpoint ~scope ~poly l =
   do_program_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 do_cofixpoint ~scope ~poly fixl =
+  let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl 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..a851e4dff5 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -1,11 +1,21 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Vernacexpr
 
 (** Special Fixpoint handling when command is activated. *)
 
 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..15f9e0328c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -402,16 +402,19 @@ 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
+            {fname = fst id_decl; univs = snd 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 ->
+        { {fname = fst id_decl; univs = snd 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..e25118e0a8 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 { fname; univs; 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 (fname,univs) ++ 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 {fname; univs; binders; rtype; body_def; notations } =
+          pr_ident_decl (fname,univs) ++ 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..6c048c7d83 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 { fname } -> Dumpglob.dump_definition fname 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 { fname } -> Dumpglob.dump_definition fname 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..6f09d9a39b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -128,18 +128,26 @@ 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 =
+  { fname : lident
+  ; univs : universe_decl_expr option
+  ; 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 +291,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