Merge PR #11016: [proof] Remove duplication in the proof save path.

Reviewed-by: SkySkimmer
Reviewed-by: herbelin

7 files changed, 255 insertions, 261 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b6843eab33..65dffb3c0b 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 =
@@ -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 2b6f987fa6..39fd332184 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -45,32 +45,51 @@ end
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Declare.Internal.get_fix_exn ce in
-  let gr = match scope with
+  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
-      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 () = 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
+
+(* Preparing proof entries *)
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1bb6620886..c668ab2ac4 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -49,17 +49,14 @@ val declare_definition
   -> Impargs.manual_implicits
   -> GlobRef.t
 
-val declare_fix
-  :  ?opaque:bool
-  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
+val declare_assumption
+  :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> 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
+  -> hook:Hook.t option
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Entries.parameter_entry
   -> GlobRef.t
 
 val prepare_definition
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 *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 68f4f55d0e..231bdafce9 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
 
@@ -49,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
     }
@@ -136,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
@@ -144,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
 
@@ -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
@@ -175,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
@@ -185,132 +178,167 @@ 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), is_opaque cb)
-  | _ -> assert false
-
-(* 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 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)
-  | 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
+(* 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 : info:Info.t -> Entries.parameter_entry -> t
+
+  val adjust_guardness_conditions
+    : info:Info.t
+    -> Evd.side_effects Declare.proof_entry
+    -> t
+
+  val declare_mutdef
+    (* Common to all recthms *)
+    : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+    -> poly:bool
+    -> 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
+    -> 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 =
+    { entry : et
+    ; info : Info.t
+    }
+
+  let variable ~info t = { entry = NoBody t; info }
+
+  (* 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 ~info const =
+    let entry = match info.Info.compute_guard 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 { entry; info }
+
+  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 ~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
+    | 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 ~poly ~uctx ?hook_data ~udecl ~ubind ~name { entry; info } =
+    (* At some point make this a single iteration *)
+    (* 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 ~poly ~udecl ~info ~ubind ?hook_data ~uctx ~name ~typ ~impargs entry i) 1 info.Info.other_thms
+    in r :: rs
+end
 
 (************************************************************************)
 (* 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 () = 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
+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 ~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 ~uctx ~poly ~udecl ~ubind ~name mutpe in
+  ()
 
 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 ~info:lemma.info ~uctx:universes ~udecl (sec_vars, (typ, ctx), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -319,29 +347,12 @@ 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.")
-
-(* Support for mutually proved theorems *)
+  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.")
 
-(* 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) ->
-          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
-            (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
+  let { Info.hook } = info in
   match po with
   | { name; entries=[const]; universes; udecl; poly } ->
     let name = match idopt with
@@ -349,37 +360,18 @@ let finish_proved env sigma 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 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;
-      (* 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
+      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 ~uctx:universes ~poly ~udecl ?hook_data ~ubind ~name mutpe
+      in ()
     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 +391,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 +419,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 +430,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 +445,26 @@ 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 ~uctx:universes ~udecl ~info (sec_vars, (typ, ctx), None)
 
-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
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 953faf6fdb..c78b470e3b 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 = 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
@@ -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 =