Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

6 files changed, 104 insertions, 99 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb4eabcc85..ed60b8274a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -112,14 +112,12 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
 
-open Decl_kinds
-
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
+let build_constant_by_tactic ~name ctx sign ~poly typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof evd id goal_kind goals in
+  let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
@@ -134,12 +132,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav
     let reraise = CErrors.push reraise in
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
-  let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
+let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
-  let ce, status, univs =
-    build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
+  let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
   let body, eff = Future.force ce.Proof_global.proof_entry_body in
   let (cb, ctx) =
     if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d01704926a..0626e40047 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -13,7 +13,6 @@
 open Names
 open Constr
 open Environ
-open Decl_kinds
 
 (** {6 ... } *)
 
@@ -58,15 +57,23 @@ val use_unification_heuristics : unit -> bool
     [tac]. The return boolean, if [false] indicates the use of an unsafe
     tactic. *)
 
-val build_constant_by_tactic :
-  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
-  EConstr.types -> unit Proofview.tactic -> 
-  Evd.side_effects Proof_global.proof_entry * bool *
-    UState.t
+val build_constant_by_tactic
+  :  name:Id.t
+  -> UState.t
+  -> named_context_val
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
-  EConstr.types -> unit Proofview.tactic -> 
-  constr * bool * UState.t
+val build_by_tactic
+  :  ?side_eff:bool
+  -> env
+  -> UState.t
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> constr * bool * UState.t
 
 val refine_by_tactic
   :  name:Id.t
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 47502fe402..9f2c90c375 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -118,8 +118,6 @@ type t =
   (** 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
@@ -290,14 +288,12 @@ let unfocused = is_last_focus end_of_stack_kind
 
 let start ~name ~poly sigma goals =
   let entry, proofview = Proofview.init sigma goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -305,14 +301,12 @@ let start ~name ~poly sigma goals =
 
 let dependent_start ~name ~poly goals =
   let entry, proofview = Proofview.dependent_init goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -488,15 +482,13 @@ type data =
   (** 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 data { proofview; focus_stack; entry; shelf; given_up; 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. *)
@@ -507,7 +499,7 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
   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 }
+  { sigma; goals; entry; stack; shelf; given_up; name; poly }
 
 let pr_proof p =
   let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 6ef34eed80..7e535a258c 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -47,8 +47,6 @@ type data =
   (** 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;
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4490fbdd64..ab8d87c100 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,12 +36,13 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
-type proof_object = {
-  id : Names.Id.t;
-  entries : Evd.side_effects proof_entry list;
-  persistence : Decl_kinds.goal_kind;
-  universes: UState.t;
-}
+type proof_object =
+  { name : Names.Id.t
+  ; entries : Evd.side_effects proof_entry list
+  ; poly : bool
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
 
 type opacity_flag = Opaque | Transparent
 
@@ -49,15 +50,18 @@ type t =
   { endline_tactic : Genarg.glob_generic_argument option
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
-  ; universe_decl: UState.universe_decl
-  ; strength : Decl_kinds.goal_kind
+  ; udecl: UState.universe_decl
+  (** Initial universe declarations *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
   }
 
 (*** Proof Global manipulation ***)
 
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
-let get_persistence ps = ps.strength
+
+let get_initial_euctx ps = ps.initial_euctx
 
 let map_proof f p = { p with proof = f p.proof }
 let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
@@ -68,7 +72,8 @@ let map_fold_proof_endline f ps =
     | None -> Proofview.tclUNIT ()
     | Some tac ->
       let open Geninterp in
-      let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in
+      let {Proof.poly} = Proof.data ps.proof in
+      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
       let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
       let tac = Geninterp.interp tag ist tac in
       Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
@@ -83,32 +88,33 @@ let compact_the_proof pf = map_proof Proof.compact pf
 let set_endline_tactic tac ps =
   { ps with endline_tactic = Some tac }
 
-(** [start_proof sigma id pl str goals] starts a proof of name
-    [id] with goals [goals] (a list of pairs of environment and
-    conclusion); [str] describes what kind of theorem/definition this
-    is (spiwack: for potential printing, I believe is used only by
-    closing commands and the xml plugin); [terminator] is used at the
-    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 name ?(pl=UState.default_univ_decl) kind goals =
-  { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion). The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+let start_proof ~name ~udecl ~poly sigma goals =
+  let proof = Proof.start ~name ~poly sigma goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
-  ; strength = kind
+  ; udecl
+  ; initial_euctx
   }
 
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
-  { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+let start_dependent_proof ~name ~udecl ~poly goals =
+  let proof = Proof.dependent_start ~name ~poly goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
-  ; strength = kind
+  ; udecl
+  ; initial_euctx
   }
 
 let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.universe_decl
+let get_universe_decl pf = pf.udecl
 
 let set_used_variables ps l =
   let open Context.Named.Declaration in
@@ -159,8 +165,8 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; universe_decl; strength } = ps in
-  let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let Proof.{ name; poly; entry } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
@@ -194,13 +200,13 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              the body.  So we keep the two sets distinct. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+          let univs = UState.check_mono_univ_decl ctx_body udecl in
           (initunivs, typ), ((body, univs), eff)
         else if poly && opaque && private_poly_univs () then
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let universes = UState.restrict universes used_univs in
           let typus = UState.restrict universes used_univs_typ in
-          let udecl = UState.check_univ_decl ~poly typus universe_decl in
+          let udecl = UState.check_univ_decl ~poly typus udecl in
           let ubody = Univ.ContextSet.diff
               (UState.context_set universes)
               (UState.context_set typus)
@@ -214,7 +220,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx = UState.restrict universes used_univs in
-          let univs = UState.check_univ_decl ~poly ctx universe_decl in
+          let univs = UState.check_univ_decl ~poly ctx udecl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -236,7 +242,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
               (Vars.universes_of_constr pt)
           in
           let univs = UState.restrict univs used_univs in
-          let univs = UState.check_mono_univ_decl univs universe_decl in
+          let univs = UState.check_mono_univ_decl univs udecl in
           (pt,univs),eff)
   in
   let entry_fn p (_, t) =
@@ -253,8 +259,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       proof_entry_universes = univs; }
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
-  { id = name; entries = entries; persistence = strength;
-    universes }
+  { name; entries = entries; poly; universes; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 4e1aa64e7b..54d5c2087a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -17,12 +17,14 @@ type t
 (* Should be moved into a proper view *)
 val get_proof : t -> Proof.t
 val get_proof_name : t -> Names.Id.t
-val get_persistence : t -> Decl_kinds.goal_kind
 val get_used_variables : t -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : t -> UState.universe_decl
 
+(** Get initial universe state *)
+val get_initial_euctx : t -> UState.t
+
 val compact_the_proof : t -> t
 
 (** When a proof is closed, it is reified into a [proof_object], where
@@ -43,37 +45,42 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
-type proof_object = {
-  id : Names.Id.t;
-  entries : Evd.side_effects proof_entry list;
-  persistence : Decl_kinds.goal_kind;
-  universes: UState.t;
-}
+(** When a proof is closed, it is reified into a [proof_object] *)
+type proof_object =
+  { name : Names.Id.t
+  (** name of the proof *)
+  ; entries : Evd.side_effects proof_entry list
+  (** list of the proof terms (in a form suitable for definitions). *)
+  ; poly : bool
+  (** polymorphic status *)
+  ; universes: UState.t
+  (** universe state *)
+  ; udecl : UState.universe_decl
+  (** universe declaration *)
+  }
 
 type opacity_flag = Opaque | Transparent
 
-(** [start_proof id str pl goals] starts a proof of name
-   [id] with goals [goals] (a list of pairs of environment and
-   conclusion); [str] describes what kind of theorem/definition this
-   is; [terminator] is used at the end of the proof to close the proof
-   (e.g. to declare the built constructions as a coercion or a setoid
-   morphism). The proof is started in the evar map [sigma] (which can
-   typically contain universe constraints), and with universe bindings
-   pl. *)
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion); [poly] determines if the proof is universe
+   polymorphic. The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
 val start_proof
-  :  Evd.evar_map
-  -> Names.Id.t
-  -> ?pl:UState.universe_decl
-  -> Decl_kinds.goal_kind
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
+  -> Evd.evar_map
   -> (Environ.env * EConstr.types) list
   -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof
-  :  Names.Id.t
-  -> ?pl:UState.universe_decl
-  -> Decl_kinds.goal_kind
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
   -> Proofview.telescope
   -> t