[vernacexpr] Remove duplicate fixpoint record.

We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.

This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.

10 files changed, 110 insertions, 113 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index aaaf7d5ce7..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
@@ -162,7 +172,7 @@ let build_newrecursive lnameargsardef =
   let sigma = Evd.from_env env0 in
   let (rec_sign,rec_impls) =
     List.fold_left
-      (fun (env,impls) { Vernacexpr.id_decl=({CAst.v=recname},_); binders; rtype } ->
+      (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
@@ -228,7 +238,7 @@ 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 { Vernacexpr.id_decl; binders; rtype } rt =
+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
@@ -330,7 +340,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     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 { Vernacexpr.id_decl = {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 { Vernacexpr.rtype } -> rtype) fix_rec_l in
@@ -350,7 +360,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
                  locate_ind
                  f_R_mut)
         in
-        let fname_kn { Vernacexpr.id_decl=(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!")
@@ -391,23 +401,23 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 
 let register_struct is_rec (fixpoint_exprl:  Vernacexpr.fixpoint_expr list) =
   match fixpoint_exprl with
-    | [ { Vernacexpr.id_decl=({ CAst.v=fname },pl); binders; rtype; body_def } ] when not is_rec ->
+    | [ { 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
+        ~kind:Decls.Definition univs
         binders None body (Some rtype);
        let evd,rev_pconstants =
          List.fold_left
-           (fun (evd,l) { Vernacexpr.id_decl=({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)
@@ -420,10 +430,10 @@ let register_struct is_rec (fixpoint_exprl:  Vernacexpr.fixpoint_expr list) =
        ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
-           (fun (evd,l) { Vernacexpr.id_decl=({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)
@@ -457,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
@@ -478,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
@@ -601,7 +611,10 @@ 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 = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in
+  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
@@ -622,7 +635,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
   let lemma, _is_struct =
     match fixpoint_exprl with
       | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] ->
-        let { Vernacexpr.id_decl = ({CAst.v=name},pl); binders; rtype; body_def } 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
@@ -645,10 +658,10 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
             true
         in
         if register_built
-        then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false
+        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.id_decl = ({CAst.v=name},pl); binders; rtype; body_def} 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
@@ -671,7 +684,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
             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 binders rtype body pre_hook, true
+        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 { Vernacexpr.rec_order } ->
@@ -683,9 +696,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro
                     )
             fixpoint_exprl;
         let fixpoint_exprl = recompute_binder_list fixpoint_exprl in
-        let fix_names =
-          List.map (function { Vernacexpr.id_decl=({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
@@ -878,21 +889,21 @@ let make_graph (f_ref : GlobRef.t) =
                       )
                   in
                   let b' = add_args id.CAst.v new_args b in
-                  { Vernacexpr.id_decl=(id,None)
+                  { 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 id = Label.to_id (Constant.label c) in
-           [{ Vernacexpr.id_decl=(CAst.make id,None); rec_order = None; binders=nal_tas; rtype=t; body_def=Some b; notations=[]}]
+           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.id_decl=({CAst.v=id},_) } ->
+         (fun { Vernacexpr.fname= {CAst.v=id} } ->
             add_Function false (Constant.make2 mp (Label.of_id id)))
          expr_list)
 
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 11ff6e9df9..8750a64ccc 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -106,7 +106,7 @@ let classify_vernac e =
          else GuaranteesOpacity
        in
         let ids, open_proof =
-          List.fold_left (fun (l,b) {Vernacexpr.id_decl=({CAst.v=id},_); body_def} ->
+          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)
@@ -118,7 +118,7 @@ let classify_vernac e =
          else GuaranteesOpacity
        in
         let ids, open_proof =
-          List.fold_left (fun (l,b) { Vernacexpr.id_decl=({CAst.v=id},_); body_def } ->
+          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)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b7da4f964d..74c9bc2886 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -107,27 +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 : 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
+  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)
 
@@ -136,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
 
@@ -168,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 =
+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 ->
@@ -223,7 +216,7 @@ let interp_recursive ~program_mode ~cofix fixl =
   (* 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
+      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))
@@ -318,35 +311,28 @@ 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 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 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 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 =
-  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
+(* 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 = extract_fixpoint_components ~structonly:true l in
-  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl 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
 
@@ -361,9 +347,9 @@ 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 = extract_cofixpoint_components l in
-  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
+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 =
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 1018c463c6..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} *)
@@ -33,24 +32,20 @@ val do_cofixpoint :
 (** 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
-  ; fix_notations : decl_notation list
-  }
-
 (** 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 ->
+  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,20 +55,11 @@ 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 list -> structured_fixpoint_expr 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
 
 val interp_fixpoint
   :  cofix:bool
-  -> structured_fixpoint_expr list
+  -> lident option fix_expr_gen list
   -> recursive_preentry * UState.universe_decl * UState.t *
      (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0104c99e41..c6e68effd7 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -289,19 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
   | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
-  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl 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 { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
-      [ Vernacexpr.{id_decl=({CAst.v=id},pl);binders;rtype;body_def;notations} ] ->
+      [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded (id, pl, binders, rtype, out_def body_def) poly r recarg notations
+        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
-      [Vernacexpr.{id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations }] ->
+      [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 ->
@@ -311,13 +311,15 @@ 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, binders, rtype, out_def body_def) poly
+        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 = 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
+      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"
@@ -332,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 = extract_cofixpoint_components l in
+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 fa3d2b7020..a851e4dff5 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -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 Vernacexpr
 
 (** Special Fixpoint handling when command is activated. *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 678d4436d2..15f9e0328c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -407,13 +407,14 @@ GRAMMAR EXTEND Gram
         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}
+            {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
           } ] ]
   ;
   corec_definition:
     [ [ 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} } ] ]
+        { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
+        } ]]
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> { c }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 835f5e0b75..e25118e0a8 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -419,12 +419,12 @@ 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 { id_decl; rec_order; binders; rtype; body_def; notations } =
+  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) binders rec_order in
-    pr_ident_decl id_decl ++ pr_binders_arg binders ++ annot
+    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
@@ -858,8 +858,8 @@ let string_of_definition_object_kind = let open Decls in function
           | DoDischarge -> keyword "Let" ++ spc ()
           | NoDischarge -> str ""
         in
-        let pr_onecorec {id_decl; binders; rtype; body_def; notations } =
-          pr_ident_decl id_decl ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
+        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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0205a653c5..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 { id_decl = (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 { id_decl = (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 =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8b8123bd30..6f09d9a39b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -131,7 +131,8 @@ type definition_expr =
 type decl_notation = lstring * constr_expr * scope_name option
 
 type 'a fix_expr_gen =
-  { id_decl : ident_decl
+  { fname : lident
+  ; univs : universe_decl_expr option
   ; rec_order : 'a
   ; binders : local_binder_expr list
   ; rtype : constr_expr