From 599f61a45769d5938758e0fcbd479b9c8f493a58 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Jun 2019 18:51:39 +0200
Subject: [lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.

Key information about an interactive lemma proof was stored as a
closure on an ad-hoc hook, then later made available to the hook
closing actions.

Instead, we put this information in the lemma state and incorporate
these declarations into the normal save path.

We prepare to put the information about rec_thms in the state too.
---
 proofs/pfedit.ml        | 2 +-
 proofs/proof_global.ml  | 8 ++++----
 proofs/proof_global.mli | 4 ++--
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb4eabcc85..d00f2c4803 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,7 +119,7 @@ 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 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 evd id UState.default_univ_decl goal_kind goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4490fbdd64..dfd54594eb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -91,19 +91,19 @@ let set_endline_tactic tac ps =
     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 =
+let start_proof sigma name udecl kind goals =
   { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
+  ; universe_decl = udecl
   ; strength = kind
   }
 
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
+let start_dependent_proof name udecl kind goals =
   { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
+  ; universe_decl = udecl
   ; strength = kind
   }
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 4e1aa64e7b..17f5c73560 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -63,7 +63,7 @@ type opacity_flag = Opaque | Transparent
 val start_proof
   :  Evd.evar_map
   -> Names.Id.t
-  -> ?pl:UState.universe_decl
+  -> UState.universe_decl
   -> Decl_kinds.goal_kind
   -> (Environ.env * EConstr.types) list
   -> t
@@ -72,7 +72,7 @@ val start_proof
     initial goals. *)
 val start_dependent_proof
   :  Names.Id.t
-  -> ?pl:UState.universe_decl
+  -> UState.universe_decl
   -> Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t
-- 
cgit v1.2.3


From fb92bcc7830a084a4a204c4f58c44e83c180a9c9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 May 2019 06:43:46 +0200
Subject: [proof] Remove redundant universe declaration information.

This was already in the base proof object however not forwarded by
`close_proof`. thus it had to be stored twice.

There are more cases like this, like `poly`, all are covered by
subsequent commits.
---
 proofs/proof_global.ml  | 34 +++++++++++++++++-----------------
 proofs/proof_global.mli | 13 +++++++------
 2 files changed, 24 insertions(+), 23 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index dfd54594eb..2f7e5d618a 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 =
+  { id : Names.Id.t
+  ; entries : Evd.side_effects proof_entry list
+  ; persistence : Decl_kinds.goal_kind
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
 
 type opacity_flag = Opaque | Transparent
 
@@ -49,7 +50,7 @@ type t =
   { endline_tactic : Genarg.glob_generic_argument option
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
-  ; universe_decl: UState.universe_decl
+  ; udecl: UState.universe_decl
   ; strength : Decl_kinds.goal_kind
   }
 
@@ -95,7 +96,7 @@ let start_proof sigma name udecl kind goals =
   { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = udecl
+  ; udecl
   ; strength = kind
   }
 
@@ -103,12 +104,12 @@ let start_dependent_proof name udecl kind goals =
   { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = udecl
+  ; udecl
   ; strength = kind
   }
 
 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,7 +160,7 @@ 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 { section_vars; proof; udecl; strength } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -194,13 +195,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 +215,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 +237,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 +254,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 }
+  { id = name; entries = entries; persistence = strength; 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 17f5c73560..3baa58084d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -43,12 +43,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 =
+  { id : Names.Id.t
+  ; entries : Evd.side_effects proof_entry list
+  ; persistence : Decl_kinds.goal_kind
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
 
 type opacity_flag = Opaque | Transparent
 
-- 
cgit v1.2.3


From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 May 2019 05:33:10 +0200
Subject: [proof] Remove duplicated universe polymorphic from decl_kinds

This information is already present on `Proof.t`, so we extract it
form there.

Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
---
 proofs/pfedit.ml        |  8 ++++----
 proofs/pfedit.mli       | 16 ++++++++++------
 proofs/proof_global.ml  | 14 ++++++++------
 proofs/proof_global.mli |  3 +++
 4 files changed, 25 insertions(+), 16 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d00f2c4803..64d21be7e8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -116,10 +116,10 @@ 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 id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) 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 UState.default_univ_decl goal_kind goals in
+  let pf = Proof_global.start_proof evd id ~poly UState.default_univ_decl goal_kind goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
@@ -137,9 +137,9 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav
 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 sign = val_of_named_context (named_context env) in
-  let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
+  let gk = Global ImportDefaultBehavior, Proof Theorem in
   let ce, status, univs =
-    build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
+    build_constant_by_tactic id sigma sign ~poly ~goal_kind:gk 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..51cb3ca0ee 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -58,14 +58,18 @@ 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
+  :  Id.t
+  -> UState.t
+  -> named_context_val
+  -> poly:bool
+  -> ?goal_kind:goal_kind
+  -> 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 -> 
+  EConstr.types -> unit Proofview.tactic ->
   constr * bool * UState.t
 
 val refine_by_tactic
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2f7e5d618a..22f818edbb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -39,6 +39,7 @@ type 'a proof_entry = {
 type proof_object =
   { id : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
+  ; poly : bool
   ; persistence : Decl_kinds.goal_kind
   ; universes: UState.t
   ; udecl : UState.universe_decl
@@ -69,7 +70,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 ())
@@ -92,16 +94,16 @@ let set_endline_tactic tac ps =
     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 udecl kind goals =
-  { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+let start_proof sigma name udecl ~poly kind goals =
+  { proof = Proof.start ~name ~poly sigma goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
   ; strength = kind
   }
 
-let start_dependent_proof name udecl kind goals =
-  { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+let start_dependent_proof name udecl ~poly kind goals =
+  { proof = Proof.dependent_start ~name ~poly goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
@@ -254,7 +256,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; udecl }
+  { id = name; entries = entries; poly; persistence = strength; 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 3baa58084d..5bfed948ba 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,6 +46,7 @@ type 'a proof_entry = {
 type proof_object =
   { id : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
+  ; poly : bool
   ; persistence : Decl_kinds.goal_kind
   ; universes: UState.t
   ; udecl : UState.universe_decl
@@ -65,6 +66,7 @@ val start_proof
   :  Evd.evar_map
   -> Names.Id.t
   -> UState.universe_decl
+  -> poly:bool
   -> Decl_kinds.goal_kind
   -> (Environ.env * EConstr.types) list
   -> t
@@ -74,6 +76,7 @@ val start_proof
 val start_dependent_proof
   :  Names.Id.t
   -> UState.universe_decl
+  -> poly:bool
   -> Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t
-- 
cgit v1.2.3


From 70a11c78e790d7f2f4175d1002e08f79d3ed8486 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 06:01:14 +0200
Subject: [proof] More uniformity in proof start labels.

---
 proofs/pfedit.ml        |  2 +-
 proofs/proof_global.ml  |  4 ++--
 proofs/proof_global.mli | 14 +++++++-------
 3 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 64d21be7e8..98002de119 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,7 +119,7 @@ let next = let n = ref 0 in fun () -> incr n; !n
 let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) 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 ~poly UState.default_univ_decl goal_kind goals in
+  let pf = Proof_global.start_proof ~name:id ~poly ~udecl:UState.default_univ_decl ~kind:goal_kind evd goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 22f818edbb..8ac4435539 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -94,7 +94,7 @@ let set_endline_tactic tac ps =
     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 udecl ~poly kind goals =
+let start_proof ~name ~udecl ~poly ~kind sigma goals =
   { proof = Proof.start ~name ~poly sigma goals
   ; endline_tactic = None
   ; section_vars = None
@@ -102,7 +102,7 @@ let start_proof sigma name udecl ~poly kind goals =
   ; strength = kind
   }
 
-let start_dependent_proof name udecl ~poly kind goals =
+let start_dependent_proof ~name ~udecl ~poly ~kind goals =
   { proof = Proof.dependent_start ~name ~poly goals
   ; endline_tactic = None
   ; section_vars = None
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 5bfed948ba..2c328bcf12 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -63,21 +63,21 @@ type opacity_flag = Opaque | Transparent
    typically contain universe constraints), and with universe bindings
    pl. *)
 val start_proof
-  :  Evd.evar_map
-  -> Names.Id.t
-  -> UState.universe_decl
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
   -> poly:bool
-  -> Decl_kinds.goal_kind
+  -> kind:Decl_kinds.goal_kind
+  -> 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
-  -> UState.universe_decl
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
   -> poly:bool
-  -> Decl_kinds.goal_kind
+  -> kind:Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t
 
-- 
cgit v1.2.3


From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 06:09:24 +0200
Subject: [lemmas] [proof] Split proof kinds into per-layer components.

We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:

- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
  pushed upwards]

We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.

More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
---
 proofs/pfedit.ml        | 12 ++++--------
 proofs/pfedit.mli       |  3 +--
 proofs/proof_global.ml  | 26 +++++++++-----------------
 proofs/proof_global.mli |  4 ----
 4 files changed, 14 insertions(+), 31 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 98002de119..7af14d099c 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 ~poly ?(goal_kind = Global ImportDefaultBehavior, 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 ~name:id ~poly ~udecl:UState.default_univ_decl ~kind:goal_kind evd 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
@@ -135,11 +133,9 @@ let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaul
     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 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, Proof Theorem in
-  let ce, status, univs =
-    build_constant_by_tactic id sigma sign ~poly ~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 51cb3ca0ee..d1d20b9efe 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -59,11 +59,10 @@ val use_unification_heuristics : unit -> bool
     tactic. *)
 
 val build_constant_by_tactic
-  :  Id.t
+  :  name:Id.t
   -> UState.t
   -> named_context_val
   -> poly:bool
-  -> ?goal_kind:goal_kind
   -> EConstr.types
   -> unit Proofview.tactic
   -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8ac4435539..59ece4296b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -40,7 +40,6 @@ type proof_object =
   { id : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
   ; poly : bool
-  ; persistence : Decl_kinds.goal_kind
   ; universes: UState.t
   ; udecl : UState.universe_decl
   }
@@ -52,14 +51,12 @@ type t =
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
   ; udecl: UState.universe_decl
-  ; strength : Decl_kinds.goal_kind
   }
 
 (*** 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 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
@@ -86,28 +83,23 @@ 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 ~name ~udecl ~poly ~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 =
   { proof = Proof.start ~name ~poly sigma goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
-  ; strength = kind
   }
 
-let start_dependent_proof ~name ~udecl ~poly ~kind goals =
+let start_dependent_proof ~name ~udecl ~poly goals =
   { proof = Proof.dependent_start ~name ~poly goals
   ; endline_tactic = None
   ; section_vars = None
   ; udecl
-  ; strength = kind
   }
 
 let get_used_variables pf = pf.section_vars
@@ -162,7 +154,7 @@ 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; udecl; strength } = ps in
+  let { section_vars; proof; udecl } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -256,7 +248,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; poly; persistence = strength; universes; udecl }
+  { id = 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 2c328bcf12..b402008361 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -17,7 +17,6 @@ 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. *)
@@ -47,7 +46,6 @@ type proof_object =
   { id : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
   ; poly : bool
-  ; persistence : Decl_kinds.goal_kind
   ; universes: UState.t
   ; udecl : UState.universe_decl
   }
@@ -66,7 +64,6 @@ val start_proof
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
   -> poly:bool
-  -> kind:Decl_kinds.goal_kind
   -> Evd.evar_map
   -> (Environ.env * EConstr.types) list
   -> t
@@ -77,7 +74,6 @@ val start_dependent_proof
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
   -> poly:bool
-  -> kind:Decl_kinds.goal_kind
   -> Proofview.telescope
   -> t
 
-- 
cgit v1.2.3


From 9d65c49f05f946557df4c67b6e752f978e1e9352 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Jun 2019 15:10:50 +0200
Subject: [api] Remove `polymorphic` type alias, use labels instead.

This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
---
 proofs/pfedit.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d1d20b9efe..5f8a073bd1 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -13,7 +13,6 @@
 open Names
 open Constr
 open Environ
-open Decl_kinds
 
 (** {6 ... } *)
 
@@ -67,7 +66,7 @@ val build_constant_by_tactic
   -> 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 ->
+val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:bool ->
   EConstr.types -> unit Proofview.tactic ->
   constr * bool * UState.t
 
-- 
cgit v1.2.3


From 0c47ebf825690675cbb71153b8c9e4f7f6858984 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 11 Jun 2019 02:02:15 +0200
Subject: [proof] API Documentation fixes.

---
 proofs/proof_global.ml  |  4 ++--
 proofs/proof_global.mli | 22 +++++++++++++---------
 2 files changed, 15 insertions(+), 11 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 59ece4296b..bda83487f1 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -37,7 +37,7 @@ type 'a proof_entry = {
 }
 
 type proof_object =
-  { id : Names.Id.t
+  { name : Names.Id.t
   ; entries : Evd.side_effects proof_entry list
   ; poly : bool
   ; universes: UState.t
@@ -248,7 +248,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; poly; universes; udecl }
+  { 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 b402008361..3ce46830fd 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -42,24 +42,28 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
+(** When a proof is closed, it is reified into a [proof_object] *)
 type proof_object =
-  { id : Names.Id.t
+  { 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
   :  name:Names.Id.t
   -> udecl:UState.universe_decl
-- 
cgit v1.2.3


From ffaac25e993eaf103b5a66dd3b0bce7598ac8e15 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 17 Jun 2019 15:32:06 +0200
Subject: [proof] Move initial_euctx to proof_global

These are only needed when closing / admitting a proof.
---
 proofs/proof.ml         | 36 ++++++++++++++----------------------
 proofs/proof.mli        |  2 --
 proofs/proof_global.ml  | 19 +++++++++++++++----
 proofs/proof_global.mli |  3 +++
 4 files changed, 32 insertions(+), 28 deletions(-)

(limited to 'proofs')

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 bda83487f1..ab8d87c100 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -51,6 +51,9 @@ type t =
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
   ; udecl: UState.universe_decl
+  (** Initial universe declarations *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
   }
 
 (*** Proof Global manipulation ***)
@@ -58,6 +61,8 @@ type t =
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
 
+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
 
@@ -89,17 +94,23 @@ let set_endline_tactic tac ps =
    can typically contain universe constraints), and with universe
    bindings [udecl]. *)
 let start_proof ~name ~udecl ~poly sigma goals =
-  { proof = Proof.start ~name ~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
   ; udecl
+  ; initial_euctx
   }
 
 let start_dependent_proof ~name ~udecl ~poly goals =
-  { proof = Proof.dependent_start ~name ~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
   ; udecl
+  ; initial_euctx
   }
 
 let get_used_variables pf = pf.section_vars
@@ -154,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; udecl } = 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
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3ce46830fd..54d5c2087a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,6 +22,9 @@ 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
-- 
cgit v1.2.3


From c2abcaefd796b7f430f056884349b9d959525eec Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 22 Jun 2019 01:53:08 +0200
Subject: [proof] Remove last case of optional `?poly` arguments.

As noted in GitHub discussion, it is a good idea to make `poly` always
explicit, this PR does remove last case of `?(poly=false)` in the
codebase.
---
 proofs/pfedit.ml  |  2 +-
 proofs/pfedit.mli | 11 ++++++++---
 2 files changed, 9 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7af14d099c..ed60b8274a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -132,7 +132,7 @@ let build_constant_by_tactic ~name ctx sign ~poly typ tac =
     let reraise = CErrors.push reraise in
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
+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 ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5f8a073bd1..0626e40047 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -66,9 +66,14 @@ val build_constant_by_tactic
   -> unit Proofview.tactic
   -> Evd.side_effects Proof_global.proof_entry * 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 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
-- 
cgit v1.2.3