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

Reviewed-by: SkySkimmer
Reviewed-by: gares

3 files changed, 173 insertions, 170 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 ->