From e8797829a459d27975af57f88e7d4110da4fa009 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 31 Oct 2019 03:48:21 +0100
Subject: [vernac] Minor cleanup of opens in `Vernacentries`

---
 vernac/vernacentries.ml | 70 ++++++++++++++++++++++---------------------------
 1 file changed, 32 insertions(+), 38 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 953faf6fdb..b37b7de004 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -15,17 +15,10 @@ open CErrors
 open CAst
 open Util
 open Names
-open Tacmach
-open Constrintern
-open Prettyp
 open Printer
 open Goptions
 open Libnames
-open Globnames
 open Vernacexpr
-open Constrexpr
-open Redexpr
-open Lemmas
 open Locality
 open Attributes
 
@@ -128,7 +121,7 @@ let show_intro ~proof all =
   let Proof.{goals;sigma} = Proof.data proof in
   if not (List.is_empty goals) then begin
     let gl = {Evd.it=List.hd goals ; sigma = sigma; } in
-    let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
+    let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (Tacmach.pf_concl gl)) in
     if all then
       let lid = Tactics.find_intro_names l gl in
       hov 0 (prlist_with_sep  spc Id.print lid)
@@ -493,8 +486,8 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
-    let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in
-    let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in
+    let evd, (impls, ((env, ctx), imps)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in
+    let evd, (t', imps') = Constrintern.interp_type_evars_impls ~program_mode ~impls env evd t in
     let flags = Pretyping.{ all_and_fail_flags with program_mode } in
     let inference_hook = if program_mode then Some program_inference_hook else None in
     let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
@@ -510,7 +503,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   (* XXX: This nf_evar is critical too!! We are normalizing twice if
      you look at the previous lines... *)
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in
+      { Lemmas.Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in
   let () =
     let open UState in
     if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
@@ -521,7 +514,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
+  Lemmas.start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -587,15 +580,15 @@ let vernac_start_proof ~atts kind l =
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
-    save_lemma_admitted ~lemma
+    Lemmas.save_lemma_admitted ~lemma
   | Proved (opaque,idopt) ->
-    save_lemma_proved ~lemma ~opaque ~idopt
+    Lemmas.save_lemma_proved ~lemma ~opaque ~idopt
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in
-  let () = save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
+  let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -825,7 +818,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Constrexpr.AN (qualid_of_ident ?loc id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~poly l =
@@ -1543,7 +1536,7 @@ let query_command_selector ?loc = function
 let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
   let glopt = query_command_selector glopt in
   let sigma, env = get_current_context_of_args ~pstate glopt in
-  let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in
+  let sigma, c = Constrintern.interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in
   let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
   Evarconv.check_problems_are_solved env sigma;
   let sigma = Evd.minimize_universes sigma in
@@ -1562,16 +1555,16 @@ let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
         let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in
         let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in
-        print_judgment env sigma j ++
+        Prettyp.print_judgment env sigma j ++
         pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l
     | Some r ->
         let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in
         let redfun env evm c =
-          let (redfun, _) = reduction_of_red_expr env r_interp in
+          let (redfun, _) = Redexpr.reduction_of_red_expr env r_interp in
           let (_, c) = redfun env evm c in
           c
         in
-        print_eval redfun env sigma rc j
+        Prettyp.print_eval redfun env sigma rc j
   in
   pp ++ Printer.pr_universe_ctx_set sigma uctx
 
@@ -1579,20 +1572,20 @@ let vernac_declare_reduction ~local s r =
   let local = Option.default false local in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r))
+  Redexpr.declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let c,uctx = interp_constr env sigma c in
+  let c,uctx = Constrintern.interp_constr env sigma c in
   let senv = Global.safe_env() in
   let uctx = UState.context_set uctx in
   let senv = Safe_typing.push_context_set ~strict:false uctx senv in
   let c = EConstr.to_constr sigma c in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in
-  print_safe_judgment env sigma j ++
+  Prettyp.print_safe_judgment env sigma j ++
   pr_universe_ctx_set sigma uctx
 
 
@@ -1618,6 +1611,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
     (* FIXME error on non None udecl if we find the hyp. *)
     let glnumopt = query_command_selector ?loc glopt in
     let gl,id =
+      let open Constrexpr in
       match glnumopt, ref_or_by_not.v with
       | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *)
          (try get_nth_goal ~pstate 1, qualid_basename qid with _ -> raise NoHyp)
@@ -1627,7 +1621,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
             Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
                           (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
-    let hyps = pf_hyps gl in
+    let hyps = Tacmach.pf_hyps gl in
     let decl = Context.Named.lookup id hyps in
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
@@ -1638,16 +1632,16 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
   with (* fallback to globals *)
     | NoHyp | Not_found ->
     let sigma, env = get_current_or_global_context ~pstate in
-    print_about env sigma ref_or_by_not udecl
+    Prettyp.print_about env sigma ref_or_by_not udecl
 
 let vernac_print ~pstate ~atts =
   let sigma, env = get_current_or_global_context ~pstate in
   function
   | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ()))
   | PrintTables -> print_tables ()
-  | PrintFullContext-> print_full_context_typ env sigma
-  | PrintSectionContext qid -> print_sec_context_typ env sigma qid
-  | PrintInspect n -> inspect env sigma n
+  | PrintFullContext-> Prettyp.print_full_context_typ env sigma
+  | PrintSectionContext qid -> Prettyp.print_sec_context_typ env sigma qid
+  | PrintInspect n -> Prettyp.inspect env sigma n
   | PrintGrammar ent -> Metasyntax.pr_grammar ent
   | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
@@ -1660,7 +1654,7 @@ let vernac_print ~pstate ~atts =
   | PrintDebugGC -> Mltop.print_gc ()
   | PrintName (qid,udecl) ->
     dump_global qid;
-    print_name env sigma qid udecl
+    Prettyp.print_name env sigma qid udecl
   | PrintGraph -> Prettyp.print_graph ()
   | PrintClasses -> Prettyp.print_classes()
   | PrintTypeClasses -> Prettyp.print_typeclasses()
@@ -1692,11 +1686,11 @@ let vernac_print ~pstate ~atts =
     print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
   | PrintImplicit qid ->
     dump_global qid;
-    print_impargs qid
+    Prettyp.print_impargs qid
   | PrintAssumptions (o,t,r) ->
       (* Prints all the axioms and section variables used by a term *)
       let gr = smart_global r in
-      let cstr = printable_constr_of_global gr in
+      let cstr = Globnames.printable_constr_of_global gr in
       let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in
       let nassums =
         Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
@@ -1719,7 +1713,7 @@ open Search
 let interp_search_about_item env sigma =
   function
   | SearchSubPattern pat ->
-      let _,pat = intern_constr_pattern env sigma pat in
+      let _,pat = Constrintern.intern_constr_pattern env sigma pat in
       GlobSearchSubPattern pat
   | SearchString (s,None) when Id.is_valid s ->
       GlobSearchString s
@@ -1768,7 +1762,7 @@ let vernac_search ~pstate ~atts s gopt r =
     (* if goal selector is given and wrong, then let exceptions be raised. *)
     | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g
   in
-  let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in
+  let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in
   let pr_search ref env c =
     let pr = pr_global ref in
     let pp = if !search_output_name_only
@@ -1794,17 +1788,17 @@ let vernac_search ~pstate ~atts s gopt r =
       (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
        Search.prioritize_search) pr_search
 
-let vernac_locate ~pstate = function
-  | LocateAny {v=AN qid}  -> print_located_qualid qid
-  | LocateTerm {v=AN qid} -> print_located_term qid
+let vernac_locate ~pstate = let open Constrexpr in function
+  | LocateAny {v=AN qid}  -> Prettyp.print_located_qualid qid
+  | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid
   | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
   | LocateTerm {v=ByNotation (ntn, sc)} ->
     let _, env = get_current_or_global_context ~pstate in
     Notation.locate_notation
       (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc
   | LocateLibrary qid -> print_located_library qid
-  | LocateModule qid -> print_located_module qid
-  | LocateOther (s, qid) -> print_located_other s qid
+  | LocateModule qid -> Prettyp.print_located_module qid
+  | LocateOther (s, qid) -> Prettyp.print_located_other s qid
   | LocateFile f -> locate_file f
 
 let vernac_register qid r =
-- 
cgit v1.2.3


From d050094c578bdf5fc0611b808949fee28ae2a641 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 26 Oct 2019 01:13:24 +0200
Subject: [proof] Remove duplication in the proof save path.

We move towards more unification in the proof save path of interactive
and non-interactive proofs.
---
 vernac/declareDef.ml  |  46 +++++++----
 vernac/declareDef.mli |  11 +++
 vernac/lemmas.ml      | 209 ++++++++++++++++++--------------------------------
 3 files changed, 119 insertions(+), 147 deletions(-)

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 2b6f987fa6..ba4b42c4e0 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,35 +43,55 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
+let declare_definition ~name ~scope ~kind ?hook_data ?(should_suggest=false) udecl ce imps =
   let fix_exn = Declare.Internal.get_fix_exn ce in
-  let gr = match scope with
+  let dref = match scope with
   | Discharge ->
-      let () =
-        declare_variable ~name ~kind (SectionLocalDef ce)
-      in
-      Names.GlobRef.VarRef name
+    let () = declare_variable ~name ~kind (SectionLocalDef ce) in
+    if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
+    Names.GlobRef.VarRef name
   | Global local ->
-      let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
-      let gr = Names.GlobRef.ConstRef kn in
-      let () = DeclareUniv.declare_univ_binders gr udecl in
-      gr
+    let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
+    let gr = Names.GlobRef.ConstRef kn in
+    if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
+    let () = DeclareUniv.declare_univ_binders gr udecl in
+    gr
   in
-  let () = maybe_declare_manual_implicits false gr imps in
+  let () = maybe_declare_manual_implicits false dref imps in
   let () = definition_message name in
   begin
     match hook_data with
     | None -> ()
     | Some (hook, uctx, obls) ->
-      Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref = gr }
+      Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref }
   end;
-  gr
+  dref
 
 let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
   let kind = Decls.IsDefinition kind in
   declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
 
+let warn_let_as_axiom =
+  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
+    Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
+                  spc () ++ strbrk "declared as an axiom.")
+
+let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
+  let local = match scope with
+    | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
+    | Global local -> local
+  in
+  let kind = Decls.(IsAssumption Conjectural) in
+  let decl = Declare.ParameterEntry pe in
+  let kn = Declare.declare_constant ~name ~local ~kind decl in
+  let dref = Names.GlobRef.ConstRef kn in
+  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
+  let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in
+  dref
+
+(* Preparing proof entries *)
+
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
   if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1bb6620886..786169f409 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -44,6 +44,7 @@ val declare_definition
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
+  -> ?should_suggest:bool
   -> UnivNames.universe_binders
   -> Evd.side_effects Declare.proof_entry
   -> Impargs.manual_implicits
@@ -62,6 +63,16 @@ val declare_fix
   -> Impargs.manual_implicits
   -> GlobRef.t
 
+val declare_assumption
+  :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+  -> name:Id.t
+  -> scope:locality
+  -> hook:Hook.t option
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Entries.parameter_entry
+  -> GlobRef.t
+
 val prepare_definition
   :  allow_evars:bool
   -> ?opaque:bool
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 68f4f55d0e..1d3132d525 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -11,15 +11,8 @@
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
 
-open CErrors
 open Util
-open Pp
 open Names
-open Constr
-open Declareops
-open Nameops
-open Pretyping
-open Impargs
 
 module NamedDecl = Context.Named.Declaration
 
@@ -164,7 +157,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     let () = match thms with [_] -> () | _ -> assert false in
     Some (intro_tac (List.hd thms)), [] in
   match thms with
-  | [] -> anomaly (Pp.str "No proof to start.")
+  | [] -> CErrors.anomaly (Pp.str "No proof to start.")
   | { Recthm.name; typ; impargs; _}::other_thms ->
     let info =
       Info.{ hook
@@ -196,121 +189,92 @@ let retrieve_first_recthm uctx = function
     let uctx = UState.context uctx in
     let inst = Univ.UContext.instance uctx in
     let map (c, _, _) = Vars.subst_instance_constr inst c in
-    (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
+    (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), Declareops.is_opaque cb)
   | _ -> assert false
 
+let rec select_body i t =
+  let open Constr in
+  match Constr.kind t with
+  | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+  | CoFix (0,decls) -> mkCoFix (i,decls)
+  | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2)
+  | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t)
+  | App (t, args) -> mkApp (select_body i t, args)
+  | _ ->
+    CErrors.anomaly
+      Pp.(str "Not a proof by induction: " ++
+          Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
+
 (* Helper for process_recthms *)
-let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Recthm.name; typ; impargs } =
-  let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in
-  let body = Option.map EConstr.of_constr body in
-  let univs = UState.check_univ_decl ~poly uctx udecl in
-  let t_i = norm typ in
+let save_remaining_recthms ?fix_exn ~poly ~scope ~udecl ~hook uctx body opaque i { Recthm.name; typ; impargs } =
+  let sigma = Evd.from_ctx uctx in
   let kind = Decls.(IsAssumption Conjectural) in
   match body with
   | None ->
-    let open DeclareDef in
-    (match scope with
-     | Discharge ->
-       (* Let Fixpoint + Admitted gets turned into axiom so scope is Global,
-          see finish_admitted *)
-       assert false
-     | Global local ->
-       let kind = Decls.(IsAssumption Conjectural) in
-       let decl = Declare.ParameterEntry (None,(t_i,univs),None) in
-       let kn = Declare.declare_constant ~name ~local ~kind decl in
-       GlobRef.ConstRef kn, impargs)
+    let _, pe = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma udecl typ in
+    DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe
   | Some body ->
-    let body = norm body in
-    let rec body_i t = match Constr.kind t with
-      | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
-      | CoFix (0,decls) -> mkCoFix (i,decls)
-      | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
-      | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
-      | App (t, args) -> mkApp (body_i t, args)
-      | _ ->
-        anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
-    let body_i = body_i body in
-    let open DeclareDef in
-    match scope with
-    | Discharge ->
-      let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
-      let c = Declare.SectionLocalDef const in
-      let () = Declare.declare_variable ~name ~kind c in
-      GlobRef.VarRef name, impargs
-    | Global local ->
-      let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in
-      let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
-      GlobRef.ConstRef kn, impargs
-
-(* This declares implicits and calls the hooks for all the theorems,
-   including the main one *)
-let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms =
-  let other_thms_data =
-    if List.is_empty other_thms then [] else
-      (* there are several theorems defined mutually *)
-      let body,opaq = retrieve_first_recthm uctx dref in
-      List.map_i (save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq) 1 other_thms in
-  let thms_data = (dref,imps)::other_thms_data in
-  List.iter (fun (dref,imps) ->
-      maybe_declare_manual_implicits false dref imps;
-      DeclareDef.Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref})) thms_data
+    let body = EConstr.of_constr (select_body i body) in
+    (* XXX: we are normalizing twice here, entries do contain ground terms *)
+    let _, de = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:(Some typ) ~body in
+    let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+    let ubind = UnivNames.empty_binders in (* XXX fixme ubind *)
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind de impargs
+
+(* This declares implicits and calls the hooks for other_thms *)
+let process_recthms ?fix_exn ?hook uctx ~udecl ~poly ~scope dref other_thms =
+  if List.is_empty other_thms then ()
+  else
+    let body, opaque = retrieve_first_recthm uctx dref in
+    let _ = List.map_i (save_remaining_recthms ?fix_exn ~poly ~scope ~udecl ~hook uctx body opaque) 1 other_thms in
+    ()
 
 (************************************************************************)
 (* Admitting a lemma-like constant                                      *)
 (************************************************************************)
 
 (* Admitted *)
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
-                                spc () ++ strbrk "declared as an axiom.")
-
 let get_keep_admitted_vars =
   Goptions.declare_bool_option_and_ref
     ~depr:false
     ~key:["Keep"; "Admitted"; "Variables"]
     ~value:true
 
-let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs other_thms =
-  let open DeclareDef in
-  let local = match scope with
-  | Global local -> local
-  | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
-  in
-  let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in
+let compute_proof_using_for_admitted proof typ pproofs =
+  if not (get_keep_admitted_vars ()) then None
+  else match Proof_global.get_used_variables proof, pproofs with
+    | Some _ as x, _ -> x
+    | None, pproof :: _ ->
+      let env = Global.env () in
+      let ids_typ = Environ.global_vars_set env typ in
+      (* [pproof] is evar-normalized by [partial_proof]. We don't
+         count variables appearing only in the type of evars. *)
+      let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in
+      Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
+    | _ -> None
+
+let finish_admitted ~name ~poly ~scope pe uctx hook ~udecl impargs other_thms =
+  let dref = DeclareDef.declare_assumption ~name ~scope ~hook ~uctx ~impargs pe in
+  (* Should both of those be done in declare_axiom? *)
   let () = Declare.assumption_message name in
-  DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
-  (* This takes care of the implicits and hook for the current constant*)
-  process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms
+  DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx);
+  process_recthms ?fix_exn:None ?hook uctx ~udecl ~poly ~scope dref other_thms
 
 let save_lemma_admitted ~(lemma : t) : unit =
-  (* Used for printing in recthms *)
-  let env = Global.env () in
   let { Info.hook; scope; impargs; other_thms } = lemma.info in
   let udecl = Proof_global.get_universe_decl lemma.proof in
-  let Proof.{ sigma; name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
+  let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
     | [typ] -> snd typ
-    | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
+    | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
   in
   let typ = EConstr.Unsafe.to_constr typ in
   let proof = Proof_global.get_proof lemma.proof in
   let pproofs = Proof.partial_proof proof in
-  let sec_vars =
-    if not (get_keep_admitted_vars ()) then None
-    else match Proof_global.get_used_variables lemma.proof, pproofs with
-      | Some _ as x, _ -> x
-      | None, pproof :: _ ->
-        let env = Global.env () in
-        let ids_typ = Environ.global_vars_set env typ in
-        (* [pproof] is evar-normalized by [partial_proof]. We don't
-           count variables appearing only in the type of evars. *)
-        let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in
-        Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
-      | _ -> None in
+  let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in
-  finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+  finish_admitted ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -319,8 +283,8 @@ let save_lemma_admitted ~(lemma : t) : unit =
 let default_thm_id = Id.of_string "Unnamed_thm"
 
 let check_anonymity id save_ident =
-  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
-    user_err Pp.(str "This command can only be used for unnamed theorem.")
+  if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then
+    CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.")
 
 (* Support for mutually proved theorems *)
 
@@ -332,14 +296,15 @@ let adjust_guardness_conditions const = function
     let env = Global.env() in
     Declare.Internal.map_entry_body const
       ~f:(fun ((body, ctx), eff) ->
+          let open Constr in
           match Constr.kind body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
             let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
-            let indexes = search_guard env possible_indexes fixdecls in
+            let indexes = Pretyping.search_guard env possible_indexes fixdecls in
             (mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff)
 
-let finish_proved env sigma idopt po info =
+let finish_proved idopt po info =
   let open Proof_global in
   let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
   match po with
@@ -352,34 +317,18 @@ let finish_proved env sigma idopt po info =
       let const = adjust_guardness_conditions const compute_guard in
       let should_suggest = const.Declare.proof_entry_opaque &&
                            Option.is_empty const.Declare.proof_entry_secctx in
-      let open DeclareDef in
-      let r = match scope with
-        | Discharge ->
-          let c = Declare.SectionLocalDef const in
-          let () = Declare.declare_variable ~name ~kind c in
-          let () = if should_suggest
-            then Proof_using.suggest_variable (Global.env ()) name
-          in
-          GlobRef.VarRef name
-        | Global local ->
-          let kn =
-            Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in
-          let () = if should_suggest
-            then Proof_using.suggest_constant (Global.env ()) kn
-          in
-          let gr = GlobRef.ConstRef kn in
-          DeclareUniv.declare_univ_binders gr (UState.universe_binders universes);
-          gr
-      in
-      Declare.definition_message name;
+      let hook_data = Option.map (fun hook -> hook, universes, []) hook in
+      let ubind = UState.universe_binders universes in
+      let r : Names.GlobRef.t =
+        DeclareDef.declare_definition ~should_suggest ~name ~scope ~kind ?hook_data ubind const impargs in
       (* This takes care of the implicits and hook for the current constant*)
-      process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
+      process_recthms ~fix_exn ?hook universes ~udecl ~poly ~scope r other_thms
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
       Exninfo.iraise (fix_exn e)
     in ()
   | _ ->
-    CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
+    CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term")
 
 let finish_derived ~f ~name ~idopt ~entries =
   (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
@@ -399,7 +348,7 @@ let finish_derived ~f ~name ~idopt ~entries =
   let f_kind = Decls.(IsDefinition Definition) in
   let f_def = Declare.DefinitionEntry f_def in
   let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
-  let f_kn_term = mkConst f_kn in
+  let f_kn_term = Constr.mkConst f_kn in
   (* In the type and body of the proof of [suchthat] there can be
      references to the variable [f]. It needs to be replaced by
      references to the constant [f] declared above. This substitution
@@ -427,7 +376,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
         let id =
           match Evd.evar_ident ev sigma0 with
           | Some id -> id
-          | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
+          | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n)
         in
         let entry, args = Declare.Internal.shrink_entry local_context entry in
         let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in
@@ -438,12 +387,12 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
   in
   hook recobls sigma
 
-let finalize_proof idopt env sigma proof_obj proof_info =
+let finalize_proof idopt proof_obj proof_info =
   let open Proof_global in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
-    finish_proved env sigma idopt proof_obj proof_info
+    finish_proved idopt proof_obj proof_info
   | End_obligation oinfo ->
     DeclareObl.obligation_terminator proof_obj.entries proof_obj.universes oinfo
   | End_derive { f ; name } ->
@@ -453,35 +402,27 @@ let finalize_proof idopt env sigma proof_obj proof_info =
 
 let save_lemma_proved ~lemma ~opaque ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
-  let env = Global.env () in
-  let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
   let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in
-  finalize_proof idopt env sigma proof_obj lemma.info
+  finalize_proof idopt proof_obj lemma.info
 
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
 let save_lemma_admitted_delayed ~proof ~info =
   let open Proof_global in
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
   let { name; entries; universes; udecl; poly } = proof in
   let { Info.hook; scope; impargs; other_thms } = info in
   if List.length entries <> 1 then
-    user_err Pp.(str "Admitted does not support multiple statements");
+    CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
   let poly = match proof_entry_universes with
     | Entries.Monomorphic_entry _ -> false
     | Entries.Polymorphic_entry (_, _) -> true in
   let typ = match proof_entry_type with
-    | None -> user_err Pp.(str "Admitted requires an explicit statement");
+    | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement");
     | Some typ -> typ in
   let ctx = UState.univ_entry ~poly universes in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+  finish_admitted ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
-let save_lemma_proved_delayed ~proof ~info ~idopt =
-  (* Env and sigma are just used for error printing in save_remaining_recthms *)
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  finalize_proof idopt env sigma proof info
+let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info
-- 
cgit v1.2.3


From c9f7a31ef67ce638ec591f9e5760941706bc12bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 19:08:22 -0500
Subject: [save proof] Declare universe_binders unconditionally for mutual
 assumptions.

As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.
---
 vernac/declareDef.ml | 2 ++
 vernac/lemmas.ml     | 3 ---
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index ba4b42c4e0..bd857a6e38 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -87,6 +87,8 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
   let kn = Declare.declare_constant ~name ~local ~kind decl in
   let dref = Names.GlobRef.ConstRef kn in
   let () = Impargs.maybe_declare_manual_implicits false dref impargs in
+  let () = Declare.assumption_message name in
+  let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in
   let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in
   dref
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1d3132d525..5eacd7aca7 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -255,9 +255,6 @@ let compute_proof_using_for_admitted proof typ pproofs =
 
 let finish_admitted ~name ~poly ~scope pe uctx hook ~udecl impargs other_thms =
   let dref = DeclareDef.declare_assumption ~name ~scope ~hook ~uctx ~impargs pe in
-  (* Should both of those be done in declare_axiom? *)
-  let () = Declare.assumption_message name in
-  DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx);
   process_recthms ?fix_exn:None ?hook uctx ~udecl ~poly ~scope dref other_thms
 
 let save_lemma_admitted ~(lemma : t) : unit =
-- 
cgit v1.2.3


From 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 29 Feb 2020 15:25:42 -0500
Subject: [lemmas] Handle mutual lemmas more uniformly.

We split the paths for mutual / non-mutual constants, and we enforce
some further invariants, in particular we avoid messing around with
the body of saved constants, and using the indirect accessor.

This should be almost semantically equivalent to the previous code,
including some questionable choices present there.

In further cleanups we will move this code to Declare, which should
hopefully help clarify some of the semantics.
---
 vernac/comFixpoint.ml   |   4 +-
 vernac/declareDef.ml    |   4 +-
 vernac/declareDef.mli   |   1 -
 vernac/lemmas.ml        | 221 +++++++++++++++++++++++++++++-------------------
 vernac/lemmas.mli       |   2 +-
 vernac/vernacentries.ml |   2 +-
 6 files changed, 142 insertions(+), 92 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b6843eab33..a29d60ccde 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,8 +255,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
     | None -> Decls.CoFixpoint, true, []
   in
   let thms =
-    List.map3 (fun name t (ctx,impargs,_) ->
-        { Lemmas.Recthm.name; typ = EConstr.of_constr t
+    List.map3 (fun name typ (ctx,impargs,_) ->
+        { Lemmas.Recthm.name; typ
         ; args = List.map RelDecl.get_name ctx; impargs})
       fixnames fixtypes fiximps in
   let init_tac =
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index bd857a6e38..dea2ccb9af 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,8 +43,10 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data ?(should_suggest=false) udecl ce imps =
+let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Declare.Internal.get_fix_exn ce in
+  let should_suggest = ce.Declare.proof_entry_opaque &&
+                       Option.is_empty ce.Declare.proof_entry_secctx in
   let dref = match scope with
   | Discharge ->
     let () = declare_variable ~name ~kind (SectionLocalDef ce) in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 786169f409..17c2862cad 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -44,7 +44,6 @@ val declare_definition
   -> scope:locality
   -> kind:Decls.logical_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> ?should_suggest:bool
   -> UnivNames.universe_binders
   -> Evd.side_effects Declare.proof_entry
   -> Impargs.manual_implicits
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 5eacd7aca7..992a5945be 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -42,7 +42,7 @@ end
 module Recthm = struct
   type t =
     { name : Id.t
-    ; typ : EConstr.t
+    ; typ : Constr.t
     ; args : Name.t list
     ; impargs : Impargs.manual_implicits
     }
@@ -129,7 +129,7 @@ let start_dependent_lemma ~name ~poly
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun { Recthm.name; typ } -> name,typ) thms with
+    match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -137,7 +137,7 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with
+    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
@@ -168,7 +168,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
            ; scope
            ; kind
            } in
-    let lemma = start_lemma ~name ~poly ~udecl ~info sigma typ in
+    let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
     pf_map (Proof_global.map_proof (fun p ->
         match init_tac with
         | None -> p
@@ -178,56 +178,123 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
 (* Commom constant saving path, for both Qed and Admitted               *)
 (************************************************************************)
 
-(* Helper for process_recthms *)
-let retrieve_first_recthm uctx = function
-  | GlobRef.VarRef id ->
-    NamedDecl.get_value (Global.lookup_named id),
-    Decls.variable_opacity id
-  | GlobRef.ConstRef cst ->
-    let cb = Global.lookup_constant cst in
-    (* we get the right order somehow but surely it could be enforced in a better way *)
-    let uctx = UState.context uctx in
-    let inst = Univ.UContext.instance uctx in
-    let map (c, _, _) = Vars.subst_instance_constr inst c in
-    (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), Declareops.is_opaque cb)
-  | _ -> assert false
-
-let rec select_body i t =
-  let open Constr in
-  match Constr.kind t with
-  | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
-  | CoFix (0,decls) -> mkCoFix (i,decls)
-  | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2)
-  | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t)
-  | App (t, args) -> mkApp (select_body i t, args)
-  | _ ->
-    CErrors.anomaly
-      Pp.(str "Not a proof by induction: " ++
-          Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
-
-(* Helper for process_recthms *)
-let save_remaining_recthms ?fix_exn ~poly ~scope ~udecl ~hook uctx body opaque i { Recthm.name; typ; impargs } =
-  let sigma = Evd.from_ctx uctx in
-  let kind = Decls.(IsAssumption Conjectural) in
-  match body with
-  | None ->
-    let _, pe = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma udecl typ in
-    DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe
-  | Some body ->
-    let body = EConstr.of_constr (select_body i body) in
-    (* XXX: we are normalizing twice here, entries do contain ground terms *)
-    let _, de = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:(Some typ) ~body in
-    let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-    let ubind = UnivNames.empty_binders in (* XXX fixme ubind *)
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind de impargs
-
-(* This declares implicits and calls the hooks for other_thms *)
-let process_recthms ?fix_exn ?hook uctx ~udecl ~poly ~scope dref other_thms =
-  if List.is_empty other_thms then ()
-  else
-    let body, opaque = retrieve_first_recthm uctx dref in
-    let _ = List.map_i (save_remaining_recthms ?fix_exn ~poly ~scope ~udecl ~hook uctx body opaque) 1 other_thms in
-    ()
+(* Support for mutually proved theorems *)
+
+(* XXX: Most of this does belong to Declare, due to proof_entry manip *)
+module MutualEntry : sig
+
+  (* We keep this type abstract and to avoid uncontrolled hacks *)
+  type t
+
+  val variable : other_thms:Recthm.t list -> Entries.parameter_entry -> t
+
+  val adjust_guardness_conditions
+    : other_thms:Recthm.t list
+    -> possible_indexes:int list list
+    -> Evd.side_effects Declare.proof_entry
+    -> t
+
+  val declare_mutdef
+    (* Common to all recthms *)
+    : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+    -> scope:DeclareDef.locality
+    -> poly:bool
+    -> kind:Decls.logical_kind
+    -> hook:DeclareDef.Hook.t option
+    -> uctx:UState.t
+    -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list
+    -> udecl:UState.universe_decl
+    (* Only for the first constant, introduced by compat *)
+    -> ubind:UnivNames.universe_binders
+    -> name:Id.t
+    -> impargs:Impargs.manual_implicits
+    -> t
+    -> Names.GlobRef.t list
+
+end = struct
+
+  (* Body with the fix *)
+  type et =
+    | NoBody of Entries.parameter_entry
+    | Single of Evd.side_effects Declare.proof_entry
+    | Mutual of Evd.side_effects Declare.proof_entry
+
+  type t =
+    { other_thms : Recthm.t list
+    ; entry : et
+    }
+
+  let variable ~other_thms t = { other_thms; entry = NoBody t }
+
+  (* XXX: Refactor this with the code in
+     [ComFixpoint.declare_fixpoint_generic] *)
+  let guess_decreasing env possible_indexes ((body, ctx), eff) =
+    let open Constr in
+    match Constr.kind body with
+    | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+      let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
+      let indexes = Pretyping.search_guard env possible_indexes fixdecls in
+      (mkFix ((indexes,0),fixdecls), ctx), eff
+    | _ -> (body, ctx), eff
+
+  let adjust_guardness_conditions ~other_thms ~possible_indexes const =
+    let entry = match possible_indexes with
+    | [] ->
+      (* Not a recursive statement *)
+      Single const
+    | possible_indexes ->
+      (* Try all combinations... not optimal *)
+      let env = Global.env() in
+      let pe = Declare.Internal.map_entry_body const
+          ~f:(guess_decreasing env possible_indexes)
+      in
+      Mutual pe
+    in { other_thms; entry }
+
+  let rec select_body i t =
+    let open Constr in
+    match Constr.kind t with
+    | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+    | CoFix (0,decls) -> mkCoFix (i,decls)
+    | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2)
+    | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t)
+    | App (t, args) -> mkApp (select_body i t, args)
+    | _ ->
+      CErrors.anomaly
+        Pp.(str "Not a proof by induction: " ++
+            Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
+
+  let declare_mutdef ?fix_exn ~scope ~poly ~kind ~hook ~uctx ?hook_data ~udecl ~ubind ?typ ~name ~impargs mutpe i =
+    match mutpe with
+    | NoBody pe ->
+      DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe
+    | Single pe ->
+      (* We'd like to do [assert (i = 0)] here, however this codepath
+         is used when declaring mutual cofixpoints *)
+      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
+    | Mutual pe ->
+      (* if typ = None , we don't touch the type; used in the base case *)
+      let pe =
+        match typ with
+        | None -> pe
+        | Some typ ->
+          Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ)
+      in
+      let pe = Declare.Internal.map_entry_body pe
+          ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in
+      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
+
+  let declare_mutdef ?fix_exn ~scope ~poly ~kind ~hook ~uctx ?hook_data ~udecl ~ubind ~name ~impargs { other_thms ; entry } =
+    (* At some point make this a single iteration *)
+    let r = declare_mutdef ?fix_exn ~poly ~scope ~udecl ~kind ~ubind ~hook ?hook_data ~uctx ~name ~impargs entry 0 in
+    (* Before we used to do this, check if that's right *)
+    let ubind = UnivNames.empty_binders in
+    let rs =
+      List.map_i (
+        fun i { Recthm.name; typ; impargs } ->
+          declare_mutdef ?fix_exn ~name ~poly ~scope ~udecl ~kind ~ubind ~hook ?hook_data ~uctx ~impargs ~typ entry i) 1 other_thms
+    in r :: rs
+end
 
 (************************************************************************)
 (* Admitting a lemma-like constant                                      *)
@@ -253,12 +320,15 @@ let compute_proof_using_for_admitted proof typ pproofs =
       Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
     | _ -> None
 
-let finish_admitted ~name ~poly ~scope pe uctx hook ~udecl impargs other_thms =
-  let dref = DeclareDef.declare_assumption ~name ~scope ~hook ~uctx ~impargs pe in
-  process_recthms ?fix_exn:None ?hook uctx ~udecl ~poly ~scope dref other_thms
+let finish_admitted ~name ~poly ~scope ~kind ~uctx ~hook ~udecl ~impargs ~other_thms pe =
+  let mutpe = MutualEntry.variable ~other_thms pe in
+  let ubind = UnivNames.empty_binders in
+  let _r : Names.GlobRef.t list =
+    MutualEntry.declare_mutdef ~scope ~kind ~uctx ~poly ~udecl ~hook ~ubind ~name ~impargs mutpe in
+  ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
-  let { Info.hook; scope; impargs; other_thms } = lemma.info in
+  let { Info.hook; scope; impargs; other_thms; kind } = lemma.info in
   let udecl = Proof_global.get_universe_decl lemma.proof in
   let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
@@ -271,7 +341,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
   let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in
-  finish_admitted ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+  finish_admitted ~name ~poly ~kind ~scope ~uctx:universes ~hook ~udecl ~impargs ~other_thms (sec_vars, (typ, ctx), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -283,24 +353,6 @@ let check_anonymity id save_ident =
   if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then
     CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.")
 
-(* Support for mutually proved theorems *)
-
-(* Helper for finish_proved *)
-let adjust_guardness_conditions const = function
-  | [] -> const (* Not a recursive statement *)
-  | possible_indexes ->
-    (* Try all combinations... not optimal *)
-    let env = Global.env() in
-    Declare.Internal.map_entry_body const
-      ~f:(fun ((body, ctx), eff) ->
-          let open Constr in
-          match Constr.kind body with
-          | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
-            let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
-            let indexes = Pretyping.search_guard env possible_indexes fixdecls in
-            (mkFix ((indexes,0),fixdecls), ctx), eff
-          | _ -> (body, ctx), eff)
-
 let finish_proved idopt po info =
   let open Proof_global in
   let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
@@ -311,15 +363,12 @@ let finish_proved idopt po info =
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Declare.Internal.get_fix_exn const in
     let () = try
-      let const = adjust_guardness_conditions const compute_guard in
-      let should_suggest = const.Declare.proof_entry_opaque &&
-                           Option.is_empty const.Declare.proof_entry_secctx in
+      let mutpe = MutualEntry.adjust_guardness_conditions ~other_thms ~possible_indexes:compute_guard const in
       let hook_data = Option.map (fun hook -> hook, universes, []) hook in
       let ubind = UState.universe_binders universes in
-      let r : Names.GlobRef.t =
-        DeclareDef.declare_definition ~should_suggest ~name ~scope ~kind ?hook_data ubind const impargs in
-      (* This takes care of the implicits and hook for the current constant*)
-      process_recthms ~fix_exn ?hook universes ~udecl ~poly ~scope r other_thms
+      let _r : Names.GlobRef.t list =
+        MutualEntry.declare_mutdef ~fix_exn ~scope ~kind ~uctx:universes ~poly ~udecl ?hook_data ~hook ~ubind ~name ~impargs mutpe
+      in ()
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
       Exninfo.iraise (fix_exn e)
@@ -408,7 +457,7 @@ let save_lemma_proved ~lemma ~opaque ~idopt =
 let save_lemma_admitted_delayed ~proof ~info =
   let open Proof_global in
   let { name; entries; universes; udecl; poly } = proof in
-  let { Info.hook; scope; impargs; other_thms } = info in
+  let { Info.hook; scope; impargs; kind; other_thms } = info in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -420,6 +469,6 @@ let save_lemma_admitted_delayed ~proof ~info =
     | Some typ -> typ in
   let ctx = UState.univ_entry ~poly universes in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+  finish_admitted ~name ~poly ~kind ~scope ~uctx:universes ~hook ~udecl ~impargs ~other_thms (sec_vars, (typ, ctx), None)
 
 let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index e790c39022..d645de1ceb 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -48,7 +48,7 @@ module Recthm : sig
   type t =
     { name : Id.t
     (** Name of theorem *)
-    ; typ : EConstr.t
+    ; typ : Constr.t
     (** Type of theorem  *)
     ; args : Name.t list
     (** Names to pre-introduce  *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b37b7de004..c78b470e3b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -503,7 +503,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   (* XXX: This nf_evar is critical too!! We are normalizing twice if
      you look at the previous lines... *)
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { Lemmas.Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in
+      { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
   let () =
     let open UState in
     if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
-- 
cgit v1.2.3


From b35dae7a6a9cc08c4bcdce7409e0ef45382b7ee1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 00:46:23 -0500
Subject: [declare] Remove trivial wrapper

In preparation for the introduction of an opaque mutual definition
type at the `Declare` level we remove the not very useful wrapper
`declare_fix`.

Now we should be ready to profit from `DeclareDef` and its handling of
common stuff such as `restrict_universe_context` and `check_univ_decl`
etc...
---
 vernac/comFixpoint.ml | 16 +++++++++-------
 vernac/declareDef.ml  |  5 -----
 vernac/declareDef.mli | 13 -------------
 vernac/declareObl.ml  | 15 +++++++--------
 4 files changed, 16 insertions(+), 33 deletions(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a29d60ccde..65dffb3c0b 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -272,8 +272,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   let indexes, cofix, fix_kind =
     match indexes with
-    | Some indexes -> indexes, false, Decls.Fixpoint
-    | None -> [], true, Decls.CoFixpoint
+    | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint)
+    | None -> [], true, Decls.(IsDefinition CoFixpoint)
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
@@ -294,11 +294,13 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
-  let pl = Evd.universe_binders evd in
-  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
-  let fixdecls = List.map mk_pure fixdecls in
-  ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx)
-            fixnames fixdecls fixtypes fiximps);
+  let udecl = Evd.universe_binders evd in
+  let _ : GlobRef.t list =
+    List.map4 (fun name body types imps ->
+        let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
+        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind udecl ce imps)
+      fixnames fixdecls fixtypes fiximps
+  in
   recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index dea2ccb9af..39fd332184 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,11 +69,6 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   end;
   dref
 
-let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
-  let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  let kind = Decls.IsDefinition kind in
-  declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
-
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 17c2862cad..c668ab2ac4 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -49,19 +49,6 @@ val declare_definition
   -> Impargs.manual_implicits
   -> GlobRef.t
 
-val declare_fix
-  :  ?opaque:bool
-  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> name:Id.t
-  -> scope:locality
-  -> kind:Decls.definition_object_kind
-  -> UnivNames.universe_binders
-  -> Entries.universes_entry
-  -> Evd.side_effects Entries.proof_output
-  -> Constr.types
-  -> Impargs.manual_implicits
-  -> GlobRef.t
-
 val declare_assumption
   :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> name:Id.t
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index dcb28b898f..eb9b896ec6 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -376,9 +376,6 @@ let compute_possible_guardness_evidences n fixbody fixtype =
     let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
     List.map_i (fun i _ -> i) 0 ctx
 
-let mk_proof c =
-  ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
-
 let declare_mutual_definition l =
   let len = List.length l in
   let first = List.hd l in
@@ -410,7 +407,6 @@ let declare_mutual_definition l =
   let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
   let fixnames = first.prg_deps in
   let opaque = first.prg_opaque in
-  let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
     | IsFixpoint wfl ->
@@ -421,20 +417,23 @@ let declare_mutual_definition l =
         Pretyping.search_guard (Global.env ()) possible_indexes fixdecls
       in
       ( Some indexes
-      , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l
+      , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l
       )
     | IsCoFixpoint ->
-      (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l)
+      (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l)
   in
   (* Declare the recursive definitions *)
   let poly = first.prg_poly in
   let scope = first.prg_scope in
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
+  let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
+  let udecl = UnivNames.empty_binders in
   let kns =
     List.map4
-      (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind
-          UnivNames.empty_binders univs)
+      (fun name body types imps ->
+         let ce = Declare.definition_entry ~opaque ~types ~univs body in
+         DeclareDef.declare_definition ~name ~scope ~kind udecl ce imps)
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
-- 
cgit v1.2.3


From 1c744339e54d108f5cfcadd830431a27776a658f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 06:48:10 -0500
Subject: [lemmas] Consolidate some declaration data on Info.t

Now that `MutualEntry` provides a more uniform interface we can reuse
`Info.t`

In the medium term we shall consolidate `Proof` / `Proof_global` and
`Lemmas` so admitted / finish are uniform too.
---
 vernac/lemmas.ml | 50 +++++++++++++++++++++++---------------------------
 1 file changed, 23 insertions(+), 27 deletions(-)

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 992a5945be..231bdafce9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -186,28 +186,23 @@ module MutualEntry : sig
   (* We keep this type abstract and to avoid uncontrolled hacks *)
   type t
 
-  val variable : other_thms:Recthm.t list -> Entries.parameter_entry -> t
+  val variable : info:Info.t -> Entries.parameter_entry -> t
 
   val adjust_guardness_conditions
-    : other_thms:Recthm.t list
-    -> possible_indexes:int list list
+    : info:Info.t
     -> Evd.side_effects Declare.proof_entry
     -> t
 
   val declare_mutdef
     (* Common to all recthms *)
     : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-    -> scope:DeclareDef.locality
     -> poly:bool
-    -> kind:Decls.logical_kind
-    -> hook:DeclareDef.Hook.t option
     -> uctx:UState.t
     -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list
     -> udecl:UState.universe_decl
     (* Only for the first constant, introduced by compat *)
     -> ubind:UnivNames.universe_binders
     -> name:Id.t
-    -> impargs:Impargs.manual_implicits
     -> t
     -> Names.GlobRef.t list
 
@@ -220,11 +215,11 @@ end = struct
     | Mutual of Evd.side_effects Declare.proof_entry
 
   type t =
-    { other_thms : Recthm.t list
-    ; entry : et
+    { entry : et
+    ; info : Info.t
     }
 
-  let variable ~other_thms t = { other_thms; entry = NoBody t }
+  let variable ~info t = { entry = NoBody t; info }
 
   (* XXX: Refactor this with the code in
      [ComFixpoint.declare_fixpoint_generic] *)
@@ -237,8 +232,8 @@ end = struct
       (mkFix ((indexes,0),fixdecls), ctx), eff
     | _ -> (body, ctx), eff
 
-  let adjust_guardness_conditions ~other_thms ~possible_indexes const =
-    let entry = match possible_indexes with
+  let adjust_guardness_conditions ~info const =
+    let entry = match info.Info.compute_guard with
     | [] ->
       (* Not a recursive statement *)
       Single const
@@ -249,7 +244,7 @@ end = struct
           ~f:(guess_decreasing env possible_indexes)
       in
       Mutual pe
-    in { other_thms; entry }
+    in { entry; info }
 
   let rec select_body i t =
     let open Constr in
@@ -264,7 +259,8 @@ end = struct
         Pp.(str "Not a proof by induction: " ++
             Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
 
-  let declare_mutdef ?fix_exn ~scope ~poly ~kind ~hook ~uctx ?hook_data ~udecl ~ubind ?typ ~name ~impargs mutpe i =
+  let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name ?typ ~impargs ~info mutpe i =
+    let { Info.hook; compute_guard; scope; kind; _ } = info in
     match mutpe with
     | NoBody pe ->
       DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe
@@ -284,15 +280,17 @@ end = struct
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in
       DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ubind pe impargs
 
-  let declare_mutdef ?fix_exn ~scope ~poly ~kind ~hook ~uctx ?hook_data ~udecl ~ubind ~name ~impargs { other_thms ; entry } =
+  let declare_mutdef ?fix_exn ~poly ~uctx ?hook_data ~udecl ~ubind ~name { entry; info } =
     (* At some point make this a single iteration *)
-    let r = declare_mutdef ?fix_exn ~poly ~scope ~udecl ~kind ~ubind ~hook ?hook_data ~uctx ~name ~impargs entry 0 in
+    (* impargs here are special too, fixed in upcoming PRs *)
+    let impargs = info.Info.impargs in
+    let r = declare_mutdef ?fix_exn ~poly ~info ~udecl ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in
     (* Before we used to do this, check if that's right *)
     let ubind = UnivNames.empty_binders in
     let rs =
       List.map_i (
         fun i { Recthm.name; typ; impargs } ->
-          declare_mutdef ?fix_exn ~name ~poly ~scope ~udecl ~kind ~ubind ~hook ?hook_data ~uctx ~impargs ~typ entry i) 1 other_thms
+          declare_mutdef ?fix_exn ~poly ~udecl ~info ~ubind ?hook_data ~uctx ~name ~typ ~impargs entry i) 1 info.Info.other_thms
     in r :: rs
 end
 
@@ -320,15 +318,14 @@ let compute_proof_using_for_admitted proof typ pproofs =
       Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
     | _ -> None
 
-let finish_admitted ~name ~poly ~scope ~kind ~uctx ~hook ~udecl ~impargs ~other_thms pe =
-  let mutpe = MutualEntry.variable ~other_thms pe in
+let finish_admitted ~name ~poly ~info ~uctx ~udecl pe =
+  let mutpe = MutualEntry.variable ~info pe in
   let ubind = UnivNames.empty_binders in
   let _r : Names.GlobRef.t list =
-    MutualEntry.declare_mutdef ~scope ~kind ~uctx ~poly ~udecl ~hook ~ubind ~name ~impargs mutpe in
+    MutualEntry.declare_mutdef ~uctx ~poly ~udecl ~ubind ~name mutpe in
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
-  let { Info.hook; scope; impargs; other_thms; kind } = lemma.info in
   let udecl = Proof_global.get_universe_decl lemma.proof in
   let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
@@ -341,7 +338,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
   let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in
-  finish_admitted ~name ~poly ~kind ~scope ~uctx:universes ~hook ~udecl ~impargs ~other_thms (sec_vars, (typ, ctx), None)
+  finish_admitted ~name ~poly ~info:lemma.info ~uctx:universes ~udecl (sec_vars, (typ, ctx), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -355,7 +352,7 @@ let check_anonymity id save_ident =
 
 let finish_proved idopt po info =
   let open Proof_global in
-  let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
+  let { Info.hook } = info in
   match po with
   | { name; entries=[const]; universes; udecl; poly } ->
     let name = match idopt with
@@ -363,11 +360,11 @@ let finish_proved idopt po info =
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Declare.Internal.get_fix_exn const in
     let () = try
-      let mutpe = MutualEntry.adjust_guardness_conditions ~other_thms ~possible_indexes:compute_guard const in
+      let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
       let hook_data = Option.map (fun hook -> hook, universes, []) hook in
       let ubind = UState.universe_binders universes in
       let _r : Names.GlobRef.t list =
-        MutualEntry.declare_mutdef ~fix_exn ~scope ~kind ~uctx:universes ~poly ~udecl ?hook_data ~hook ~ubind ~name ~impargs mutpe
+        MutualEntry.declare_mutdef ~fix_exn ~uctx:universes ~poly ~udecl ?hook_data ~ubind ~name mutpe
       in ()
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
@@ -457,7 +454,6 @@ let save_lemma_proved ~lemma ~opaque ~idopt =
 let save_lemma_admitted_delayed ~proof ~info =
   let open Proof_global in
   let { name; entries; universes; udecl; poly } = proof in
-  let { Info.hook; scope; impargs; kind; other_thms } = info in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -469,6 +465,6 @@ let save_lemma_admitted_delayed ~proof ~info =
     | Some typ -> typ in
   let ctx = UState.univ_entry ~poly universes in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~name ~poly ~kind ~scope ~uctx:universes ~hook ~udecl ~impargs ~other_thms (sec_vars, (typ, ctx), None)
+  finish_admitted ~name ~poly ~uctx:universes ~udecl ~info (sec_vars, (typ, ctx), None)
 
 let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info
-- 
cgit v1.2.3