[proof] Rework proof interface.

- deprecate the old 5-tuple accessor in favor of a view record,

- move `name` and `kind` proof data from `Proof_global` to `Proof`,
  this will prove useful in subsequent functionalizations of the
  interface, in particular this is what abstract, which lives in the
  monads, needs in order no to access global state.

- Note that `Proof.t` and `Proof_global.t` are redundant anyways.

20 files changed, 249 insertions, 142 deletions

diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
new file mode 100644
index 0000000000..f532fdfc52
--- /dev/null
+++ b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
+
+    ltac2_CI_REF=proof_rework
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    mtac2_CI_REF=proof_rework
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 6a4c7603ee..716a942d5c 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -196,12 +196,24 @@ let process_goal sigma g =
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
   { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
-let export_pre_goals pgs =
-  {
-    Interface.fg_goals       = pgs.Proof.fg_goals;
-    Interface.bg_goals       = pgs.Proof.bg_goals;
-    Interface.shelved_goals  = pgs.Proof.shelved_goals;
-    Interface.given_up_goals = pgs.Proof.given_up_goals
+let process_goal_diffs diff_goal_map oldp nsigma ng =
+  let open Evd in
+  let og_s = match oldp with
+    | Some oldp ->
+      let Proof.{ sigma=osigma } = Proof.data oldp in
+      (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
+       with Not_found -> None)
+    | None -> None
+  in
+  let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
+  { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
+
+let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process =
+  let process = List.map (process sigma) in
+  { Interface.fg_goals       = process goals
+  ; Interface.bg_goals       = List.(map (fun (lg,rg) -> process lg, process rg)) stack
+  ; Interface.shelved_goals  = process shelf
+  ; Interface.given_up_goals = process given_up
   }
 
 let goals () =
@@ -212,22 +224,9 @@ let goals () =
     if Proof_diffs.show_diffs () then begin
       let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
       let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
-
-      let process_goal_diffs nsigma ng =
-        let open Evd in
-        let og_s = match oldp with
-        | Some oldp ->
-          let (_,_,_,_,osigma) = Proof.proof oldp in
-          (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
-          with Not_found -> None) (* will appear as a new goal *)
-        | None -> None
-        in
-        let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
-        { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
-      in
-      Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
+      Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
     end else
-      Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+      Some (export_pre_goals Proof.(data newp) process_goal)
   with Proof_global.NoCurrentProof -> None;;
 
 let evars () =
@@ -235,7 +234,7 @@ let evars () =
     let doc = get_doc () in
     set_doc @@ Stm.finish ~doc;
     let pfts = Proof_global.give_me_the_proof () in
-    let all_goals, _, _, _, sigma = Proof.proof pfts in
+    let Proof.{ sigma } = Proof.data pfts in
     let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
     let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
     let el = List.map map_evar exl in
@@ -245,8 +244,8 @@ let evars () =
 let hints () =
   try
     let pfts = Proof_global.give_me_the_proof () in
-    let all_goals, _, _, _, sigma = Proof.proof pfts in
-    match all_goals with
+    let Proof.{ goals; sigma } = Proof.data pfts in
+    match goals with
     | [] -> None
     | g :: _ ->
       let env = Goal.V82.env sigma g in
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index c1a673edf0..171d51800e 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -57,7 +57,6 @@ type assumption_object_kind = Definitional | Logical | Conjectural
 
 *)
 type assumption_kind = locality * polymorphic * assumption_object_kind
-
 type definition_kind = locality * polymorphic * definition_object_kind
 
 (** Kinds used in proofs *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e626df5579..4bb52f599a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -632,7 +632,8 @@ let solve_remaining_by env sigma holes by =
       | Some evi ->
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
-        let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
+        let name, poly = Id.of_string "rewrite", false in
+        let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
         Evd.define evk (EConstr.of_constr c) sigma
     in
     List.fold_left solve sigma indep
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 284642b38c..816741b894 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2031,7 +2031,8 @@ let _ =
     let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
     let ist = { lfun = lfun; extra; } in
     let tac = interp_tactic ist tac in
-    let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
+    let name, poly = Id.of_string "ltac_sub", false in
+    let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/printing/printer.ml b/printing/printer.ml
index b80133b171..be0139da06 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -546,10 +546,10 @@ let rec pr_evars_int_hd pr sigma i = function
       (hov 0 (pr i evk evi)) ++
       (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest)
 
-let pr_evars_int sigma ~shelf ~givenup i evs =
+let pr_evars_int sigma ~shelf ~given_up i evs =
   let pr_status i =
     if List.mem i shelf then str " (shelved)"
-    else if List.mem i givenup then str " (given up)"
+    else if List.mem i given_up then str " (given up)"
     else mt () in
   pr_evars_int_hd
     (fun i evk evi ->
@@ -761,7 +761,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
 	if Evar.Map.is_empty exl then
 	  (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
 	else
-          let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in
+          let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in
 	  v 0 ((str "No more subgoals,"
                 ++ str " but there are non-instantiated existential variables:"
 	        ++ cut () ++ (hov 0 pei)
@@ -789,7 +789,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
      straightforward, but seriously, [Proof.proof] should return
      [evar_info]-s instead. *)
   let p = proof in
-  let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in
+  let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in
   let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
   let seeds = Proof.V82.top_evars p in
   begin match goals with
@@ -821,7 +821,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
      let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
      let os_map = match oproof with
        | Some op when diffs ->
-         let (_,_,_,_, osigma) = Proof.proof op in
+         let Proof.{sigma=osigma} = Proof.data op in
          let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
          Some (osigma, diff_goal_map)
        | _ -> None
@@ -834,8 +834,8 @@ let pr_open_subgoals ~proof =
   pr_open_subgoals_diff proof
 
 let pr_nth_open_subgoal ~proof n =
-  let gls,_,_,_,sigma = Proof.proof proof in
-  pr_subgoal n sigma gls
+  let Proof.{goals;sigma} = Proof.data proof in
+  pr_subgoal n sigma goals
 
 let pr_goal_by_id ~proof id =
   try
diff --git a/printing/printer.mli b/printing/printer.mli
index 357f30d1f4..fd4682a086 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -182,7 +182,7 @@ val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
-val pr_evars_int           : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars_int           : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
 val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
   Evar.Set.t -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index a381266976..b280ce909b 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -553,7 +553,7 @@ open Goal.Set
 let db_goal_map op np ng_to_og =
   let pr_goals title prf =
     Printf.printf "%s: " title;
-    let (goals,_,_,_,sigma) = Proof.proof prf in
+    let Proof.{goals;sigma} = Proof.data prf in
     List.iter (fun g -> Printf.printf "%d -> %s  " (Evar.repr g) (goal_to_evar g sigma)) goals;
     let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in
     List.iter (fun g -> Printf.printf "%d  " (Evar.repr g)) (elements gs);
@@ -626,11 +626,11 @@ let make_goal_map_i op np =
       let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in
 
       let oevar_to_og = ref StringMap.empty in
-      let (_,_,_,_,osigma) = Proof.proof op in
+      let Proof.{sigma=osigma} = Proof.data op in
       List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
           (Goal.Set.elements rem_gs);
 
-      let (_,_,_,_,nsigma) = Proof.proof np in
+      let Proof.{sigma=nsigma} = Proof.data np in
       let get_og ng =
         let nevar = goal_to_evar ng nsigma in
         let oevar = StringMap.find nevar nevar_to_oevar in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index acf5510aa0..e2b7df19de 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,7 +33,7 @@ let () = CErrors.register_handler begin function
 end
 
 let get_nth_V82_goal p i =
-  let goals,_,_,_,sigma = Proof.proof p in
+  let Proof.{ sigma; goals } = Proof.data p in
   try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
@@ -120,7 +120,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
 
 let instantiate_nth_evar_com n com = 
-  Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
+  Proof_global.simple_with_current_proof (fun _ p ->
+      Proof.V82.instantiate_evar Global.(env ())n com p)
 
 
 (**********************************************************************)
@@ -166,7 +167,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
   cb, status, univs
 
-let refine_by_tactic env sigma ty tac =
+let refine_by_tactic ~name ~poly env sigma ty tac =
   (* Save the initial side-effects to restore them afterwards. We set the
      current set of side-effects to be empty so that we can retrieve the
      ones created during the tactic invocation easily. *)
@@ -175,7 +176,7 @@ let refine_by_tactic env sigma ty tac =
   (* Save the existing goals *)
   let prev_future_goals = save_future_goals sigma in
   (* Start a proof *)
-  let prf = Proof.start sigma [env, ty] in
+  let prf = Proof.start ~name ~poly sigma [env, ty] in
   let (prf, _) =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
@@ -184,9 +185,9 @@ let refine_by_tactic env sigma ty tac =
       iraise (e, info)
   in
   (* Plug back the retrieved sigma *)
-  let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in
+  let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
   assert (stack = []);
-  let ans = match Proof.initial_goals prf with
+  let ans = match Proofview.initial_goals entry with
   | [c, _] -> c
   | _ -> assert false
   in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 155221947a..5699320af5 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -81,8 +81,13 @@ val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
   EConstr.types -> unit Proofview.tactic -> 
   constr * bool * UState.t
 
-val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
-  constr * Evd.evar_map
+val refine_by_tactic
+  :  name:Id.t
+  -> poly:bool
+  -> env -> Evd.evar_map
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> constr * Evd.evar_map
 (** A variant of the above function that handles open terms as well.
     Caveat: all effects are purged in the returned term at the end, but other
     evars solved by side-effects are NOT purged, so that unexpected failures may
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 6c13c4946a..1aeb24606b 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -105,22 +105,29 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
 
 (* Subpart of the type of proofs. It contains the parts of the proof which
    are under control of the undo mechanism *)
-type t = {
-  (* Current focused proofview *)
-  proofview: Proofview.proofview;
-  (* Entry for the proofview *)
-  entry : Proofview.entry;
-  (* History of the focusings, provides information on how
-     to unfocus the proof and the extra information stored while focusing.
-     The list is empty when the proof is fully unfocused. *)
-  focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list;
-  (* List of goals that have been shelved. *)
-  shelf : Goal.goal list;
-  (* List of goals that have been given up *)
-  given_up : Goal.goal list;
-  (* The initial universe context (for the statement) *)
-  initial_euctx : UState.t
-}
+type t =
+  { proofview: Proofview.proofview
+  (** Current focused proofview *)
+  ; entry : Proofview.entry
+  (** Entry for the proofview *)
+  ; focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list
+  (** History of the focusings, provides information on how to unfocus
+     the proof and the extra information stored while focusing.  The
+     list is empty when the proof is fully unfocused. *)
+  ; shelf : Goal.goal list
+  (** List of goals that have been shelved. *)
+  ; given_up : Goal.goal list
+  (** List of goals that have been given up *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; name : Names.Id.t
+  (** the name of the theorem whose proof is being constructed *)
+  ; poly : bool
+  (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+  }
+
+let initial_goals pf = Proofview.initial_goals pf.entry
+let initial_euctx pf = pf.initial_euctx
 
 (*** General proof functions ***)
 
@@ -141,7 +148,7 @@ let proof p =
   (goals,stack,shelf,given_up,sigma)
 
 type 'a pre_goals = {
-    fg_goals : 'a list;
+  fg_goals : 'a list;
   (** List of the focussed goals *)
   bg_goals : ('a list * 'a list) list;
   (** Zipper representing the unfocussed background goals *)
@@ -311,7 +318,7 @@ let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start sigma goals =
+let start ~name ~poly sigma goals =
   let entry, proofview = Proofview.init sigma goals in
   let pr = {
     proofview;
@@ -320,9 +327,13 @@ let start sigma goals =
     shelf = [] ;
     given_up = [];
     initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
+      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+    ; name
+    ; poly
+  } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
-let dependent_start goals =
+
+let dependent_start ~name ~poly goals =
   let entry, proofview = Proofview.dependent_init goals in
   let pr = {
     proofview;
@@ -331,7 +342,10 @@ let dependent_start goals =
     shelf = [] ;
     given_up = [];
     initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
+      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+    ; name
+    ; poly
+  } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
@@ -375,9 +389,6 @@ let return ?pid (p : t) =
     let p = unfocus end_of_stack_kind p () in
     Proofview.return p.proofview
 
-let initial_goals p = Proofview.initial_goals p.entry
-let initial_euctx p = p.initial_euctx
-
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
   { p with proofview; entry }
@@ -468,7 +479,7 @@ module V82 = struct
       { p with proofview = Proofview.V82.grab p.proofview }
 
   (* Main component of vernac command Existential *)
-  let instantiate_evar n com pr =
+  let instantiate_evar env n com pr =
     let tac =
       Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma ->
       let (evk, evi) =
@@ -487,7 +498,7 @@ module V82 = struct
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
-    let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in
+    let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
@@ -507,3 +518,37 @@ let all_goals p =
     let set = add given_up set in
     let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in
     add bgoals set
+
+type data =
+  { sigma : Evd.evar_map
+  (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
+  ; goals : Evar.t list
+  (** Focused goals *)
+  ; entry : Proofview.entry
+  (** Entry for the proofview *)
+  ; stack : (Evar.t list * Evar.t list) list
+  (** A representation of the focus stack *)
+  ; shelf : Evar.t list
+  (** A representation of the shelf  *)
+  ; given_up : Evar.t list
+  (** A representation of the given up goals  *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; name : Names.Id.t
+  (** The name of the theorem whose proof is being constructed *)
+  ; poly : bool
+  (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
+  }
+
+let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } =
+  let goals, sigma = Proofview.proofview proofview in
+  (* spiwack: beware, the bottom of the stack is used by [Proof]
+     internally, and should not be exposed. *)
+  let rec map_minus_one f = function
+    | [] -> assert false
+    | [_] -> []
+    | a::l -> f a :: (map_minus_one f l)
+  in
+  let stack =
+    map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
+  { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
diff --git a/proofs/proof.mli b/proofs/proof.mli
index aaabea3454..fd5e905a3b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -50,27 +50,70 @@ val proof : t ->
   * Goal.goal list
   * Goal.goal list
   * Evd.evar_map
+[@@ocaml.deprecated "use [Proof.data]"]
+
+val initial_goals : t -> (EConstr.constr * EConstr.types) list
+[@@ocaml.deprecated "use [Proof.data]"]
+
+val initial_euctx : t -> UState.t
+[@@ocaml.deprecated "use [Proof.data]"]
+
+type data =
+  { sigma : Evd.evar_map
+  (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
+  ; goals : Evar.t list
+  (** Focused goals *)
+  ; entry : Proofview.entry
+  (** Entry for the proofview *)
+  ; stack : (Evar.t list * Evar.t list) list
+  (** A representation of the focus stack *)
+  ; shelf : Evar.t list
+  (** A representation of the shelf  *)
+  ; given_up : Evar.t list
+  (** A representation of the given up goals  *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
+  ; name : Names.Id.t
+  (** The name of the theorem whose proof is being constructed *)
+  ; poly : bool;
+  (** polymorphism *)
+  }
+
+val data : t -> data
 
 (* Generic records structured like the return type of proof *)
 type 'a pre_goals = {
   fg_goals : 'a list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** List of the focussed goals *)
   bg_goals : ('a list * 'a list) list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** Zipper representing the unfocussed background goals *)
   shelved_goals : 'a list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** List of the goals on the shelf. *)
   given_up_goals : 'a list;
+  [@ocaml.deprecated "use [Proof.data]"]
   (** List of the goals that have been given up *)
 }
+[@@ocaml.deprecated "use [Proof.data]"]
 
-val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
-
+(* needed in OCaml 4.05.0, not needed in newer ones *)
+[@@@ocaml.warning "-3"]
+val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"]
+[@@ocaml.deprecated "use [Proof.data]"]
+[@@@ocaml.warning "+3"]
 
 (*** General proof functions ***)
-val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
-val dependent_start : Proofview.telescope -> t
-val initial_goals : t -> (EConstr.constr * EConstr.types) list
-val initial_euctx : t -> UState.t
+val start
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
+
+val dependent_start
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Proofview.telescope -> t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
@@ -177,8 +220,9 @@ val no_focused_goal : t -> bool
 
 (* the returned boolean signal whether an unsafe tactic has been
    used. In which case it is [false]. *)
-val run_tactic : Environ.env ->
-  unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
+val run_tactic
+  :  Environ.env
+  -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
 
 val maximal_unfocus : 'a focus_kind -> t -> t
 
@@ -208,7 +252,8 @@ module V82 : sig
   val grab_evars : t -> t
 
   (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
+  val instantiate_evar :
+    Environ.env -> int -> Constrexpr.constr_expr -> t -> t
 end
 
 (* returns the set of all goals in the proof *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 76a1e61ad2..2027ad4e21 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -90,14 +90,13 @@ type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
 
 type pstate = {
-  pid : Id.t;  (* the name of the theorem whose proof is being constructed *)
   terminator : proof_terminator CEphemeron.key;
   endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Constr.named_context option;
   proof : Proof.t;
-  strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
   universe_decl: UState.universe_decl;
+  strength : Decl_kinds.goal_kind;
 }
 
 type t = pstate list
@@ -142,7 +141,7 @@ end
 (*** Proof Global manipulation ***)
 
 let get_all_proof_names () =
-  List.map (function { pid = id } -> id) !pstates
+  List.map Proof.(function pf -> (data pf.proof).name) !pstates
 
 let cur_pstate () =
   match !pstates with
@@ -151,7 +150,7 @@ let cur_pstate () =
 
 let give_me_the_proof () = (cur_pstate ()).proof
 let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
-let get_current_proof_name () = (cur_pstate ()).pid
+let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name
 
 let with_current_proof f =
   match !pstates with
@@ -205,8 +204,12 @@ let check_no_pending_proof () =
        str"Use \"Abort All\" first or complete proof(s).")
   end
 
+let pf_name_eq id ps =
+  let Proof.{ name } = Proof.data ps.proof in
+  Id.equal name id
+
 let discard_gen id =
-  pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates
+  pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates
 
 let discard {CAst.loc;v=id} =
   let n = List.length !pstates in
@@ -223,9 +226,9 @@ let discard_all () = pstates := []
 (* [set_proof_mode] sets the proof mode to be used after it's called. It is
     typically called by the Proof Mode command. *)
 let set_proof_mode m id =
-  pstates :=
-    List.map (function { pid = id' } as p ->
-      if Id.equal id' id then { p with mode = m } else p) !pstates;
+  pstates := List.map
+      (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps)
+      !pstates;
   update_proof_mode ()
 
 let set_proof_mode mn =
@@ -244,28 +247,26 @@ let disactivate_current_proof_mode () =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator =
+let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
   let initial_state = {
-    pid = id;
     terminator = CEphemeron.create terminator;
-    proof = Proof.start sigma goals;
+    proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
     endline_tactic = None;
     section_vars = None;
-    strength = str;
     mode = find_proof_mode "No";
-    universe_decl = pl } in
+    universe_decl = pl;
+    strength = kind } in
   push initial_state pstates
 
-let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
+let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
   let initial_state = {
-    pid = id;
     terminator = CEphemeron.create terminator;
-    proof = Proof.dependent_start goals;
+    proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
     endline_tactic = None;
     section_vars = None;
-    strength = str;
     mode = find_proof_mode "No";
-    universe_decl = pl } in
+    universe_decl = pl;
+    strength = kind } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
@@ -301,10 +302,10 @@ let set_used_variables l =
       ctx, []
 
 let get_open_goals () =
-  let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
-  List.length gl +
+  let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).proof in
+  List.length goals +
     List.fold_left (+) 0
-    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
+    (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
     List.length shelf
 
 type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
@@ -323,12 +324,9 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) =
-  let { pid; section_vars; strength; proof; terminator; universe_decl } =
-    cur_pstate () in
+  let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in
+  let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
-  let poly = pi2 strength (* Polymorphic *) in
-  let initial_goals = Proof.initial_goals proof in
-  let initial_euctx = Proof.initial_euctx proof in
   let constrain_variables ctx =
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
   in
@@ -411,16 +409,16 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       const_entry_opaque = opaque;
       const_entry_universes = univs; }
   in
-  let entries = Future.map2 entry_fn fpl initial_goals in
-  { id = pid; entries = entries; persistence = strength;
+  let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
+  { id = name; entries = entries; persistence = strength;
     universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
 let return_proof ?(allow_partial=false) () =
- let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
+ let { proof } = cur_pstate () in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
-  let _,_,_,_, evd = Proof.proof proof in
+  let Proof.{sigma=evd} = Proof.data proof in
   let eff = Evd.eval_side_effects evd in
   (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
      side-effects... This may explain why one need to uniquize side-effects
@@ -428,7 +426,8 @@ let return_proof ?(allow_partial=false) () =
   let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
-  let initial_goals = Proof.initial_goals proof in
+  let Proof.{name=pid;entry} = Proof.data proof in
+  let initial_goals = Proofview.initial_goals entry in
   let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
@@ -455,10 +454,11 @@ let set_terminator hook =
 
 module V82 = struct
   let get_current_initial_conclusions () =
-  let { pid; strength; proof } = cur_pstate () in
-  let initial = Proof.initial_goals proof in
+  let { proof; strength } = cur_pstate () in
+  let Proof.{ name; entry } = Proof.data proof in
+  let initial = Proofview.initial_goals entry in
   let goals = List.map (fun (o, c) -> c) initial in
-    pid, (goals, strength)
+  name, (goals, strength)
 end
 
 let freeze ~marshallable =
@@ -473,7 +473,7 @@ let copy_terminators ~src ~tgt =
   assert(List.length src = List.length tgt);
   List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
 
-let update_global_env () =
+let update_global_env pf_info =
   with_current_proof (fun _ p ->
      Proof.in_proof p (fun sigma ->
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index b8af2bcd56..230a3207a8 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,12 +49,12 @@ let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.proof }) ->
-       let proof = Proof_global.proof_of_state proof in
-       let focused, r1, r2, r3, sigma = Proof.proof proof in
-       let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
-       if List.for_all (fun x -> simple_goal sigma x rest) focused
-       then `Simple focused
-       else `Not
+    let proof = Proof_global.proof_of_state proof in
+    let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
+    let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+    if List.for_all (fun x -> simple_goal sigma x rest) focused
+    then `Simple focused
+    else `Not
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
 
diff --git a/stm/stm.ml b/stm/stm.ml
index e835bdcb1e..77fb49625c 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1936,7 +1936,7 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id;
       stm_purify (fun () ->
-       let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
+       let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
        let is_ground c = Evarutil.is_ground_term sigma0 c in
        if not (
@@ -1957,7 +1957,7 @@ end = struct (* {{{ *)
         *)
         let st = Vernacstate.freeze_interp_state `No in
         ignore(stm_vernac_interp r_state_fb st ast);
-        let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
+        let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
@@ -1999,7 +1999,7 @@ end = struct (* {{{ *)
     (if time then System.with_time ~batch else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
     Proof_global.with_current_proof (fun _ p ->
-      let goals, _, _, _, _ = Proof.proof p in
+      let Proof.{goals} = Proof.data p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
         let f, assign =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index faff116af4..571ad9d160 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1516,8 +1516,8 @@ let pr_hint_term env sigma cl =
 let pr_applicable_hint () =
   let env = Global.env () in
   let pts = Proof_global.give_me_the_proof () in
-  let glss,_,_,_,sigma = Proof.proof pts in
-  match glss with
+  let Proof.{goals;sigma} = Proof.data pts in
+  match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
     pr_hint_term env sigma (Goal.V82.concl sigma g)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index caf4c1eca3..356b43ec14 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
    scheme on sort [sort]. Depending on the value of [dep_option] it will
    build a dependent lemma or a non-dependent one *)
 
-let inversion_scheme env sigma t sort dep_option inv_op =
+let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
     try find_rectype env sigma i
@@ -201,7 +201,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     user_err ~hdr:"lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
+  let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
@@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       invEnv ~init:Context.Named.empty
   end in
   let avoid = ref Id.Set.empty in
-  let _,_,_,_,sigma = Proof.proof pf in
+  let Proof.{sigma} = Proof.data pf in
   let sigma = Evd.minimize_universes sigma in
   let rec fill_holes c =
     match EConstr.kind sigma c with
@@ -236,7 +236,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   p, sigma
 
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
-  let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+  let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
   let univs =
     Evd.const_univ_entry ~poly sigma
   in
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 5cf2157044..e58b9ccac7 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -323,7 +323,8 @@ let loop_flush_all () =
 let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
 let evleq e1 e2 = CList.equal Evar.equal e1 e2
 let cproof p1 p2 =
-  let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in
+  let Proof.{goals=a1;stack=a2;shelf=a3;given_up=a4} = Proof.data p1 in
+  let Proof.{goals=b1;stack=b2;shelf=b3;given_up=b4} = Proof.data p2 in
   evleq a1 b1 &&
   CList.equal (pequal evleq evleq) a2 b2 &&
   CList.equal Evar.equal a3 b3 &&
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1a6eda446c..8f155adb8a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -483,7 +483,7 @@ let save_proof ?proof = function
             let pftree = Proof_global.give_me_the_proof () in
             let id, k, typ = Pfedit.current_proof_statement () in
             let typ = EConstr.Unsafe.to_constr typ in
-            let universes = Proof.initial_euctx pftree in
+            let universes = Proof.((data pftree).initial_euctx) in
             (* This will warn if the proof is complete *)
             let pproofs, _univs =
               Proof_global.return_proof ~allow_partial:true () in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c6c6f74152..ecfe39de09 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -82,12 +82,12 @@ let show_proof () =
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = Proof_global.give_me_the_proof () in
-  let gls,_,shelf,givenup,sigma = Proof.proof pfts in
-  pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma)
+  let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in
+  pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
 
 let show_universes () =
   let pfts = Proof_global.give_me_the_proof () in
-  let gls,_,_,_,sigma = Proof.proof pfts in
+  let Proof.{goals;sigma} = Proof.data pfts in
   let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
   Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
   str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx
@@ -96,9 +96,9 @@ let show_universes () =
 let show_intro all =
   let open EConstr in
   let pf = Proof_global.give_me_the_proof() in
-  let gls,_,_,_,sigma = Proof.proof pf in
-  if not (List.is_empty gls) then begin
-    let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
+  let Proof.{goals;sigma} = Proof.data pf 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
     if all then
       let lid = Tactics.find_intro_names l gl in
@@ -1047,8 +1047,9 @@ let vernac_set_end_tac tac =
 
 let vernac_set_used_variables e =
   let env = Global.env () in
+  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
   let tys =
-    List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+    List.map snd (initial_goals (Proof_global.give_me_the_proof ())) in
   let tys = List.map EConstr.Unsafe.to_constr tys in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
@@ -1815,8 +1816,8 @@ let vernac_global_check c =
 
 let get_nth_goal n =
   let pf = Proof_global.give_me_the_proof() in
-  let gls,_,_,_,sigma = Proof.proof pf in
-  let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
+  let Proof.{goals;sigma} = Proof.data pf in
+  let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
 
 exception NoHyp