[proof] API Documentation fixes.

6 files changed, 35 insertions, 31 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1f8bf5be22..edda2f2eef 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -324,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { id; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
-    id, entry, hook
+    name, entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
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
diff --git a/stm/stm.ml b/stm/stm.ml
index b73d3dcdeb..28d5447c44 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1735,7 +1735,7 @@ end = struct (* {{{ *)
     | `OK (po,_) ->
         let con =
           Nametab.locate_constant
-            (Libnames.qualid_of_ident po.Proof_global.id) in
+            (Libnames.qualid_of_ident po.Proof_global.name) in
         let c = Global.lookup_constant con in
         let o = match c.Declarations.const_body with
           | Declarations.OpaqueDef o -> o
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 75fd5dcf5b..3934a29413 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -33,7 +33,7 @@ module Hook : sig
       -> locality
       (**  [locality]: Locality of the original declaration *)
       -> GlobRef.t
-      (** [ref]: identifier of the origianl declaration *)
+      (** [ref]: identifier of the original declaration *)
       -> unit
   end
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 88a4491112..2dbcce2399 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -477,14 +477,14 @@ let get_keep_admitted_vars =
     ~key:["Keep"; "Admitted"; "Variables"]
     ~value:true
 
-let finish_admitted env sigma id ~poly ~scope pe ctx hook ~udecl impargs other_thms =
+let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs other_thms =
   let open DeclareDef in
   let local = match scope with
   | Global local -> local
-  | Discharge -> warn_let_as_axiom id; ImportNeedQualified
+  | Discharge -> warn_let_as_axiom name; ImportNeedQualified
   in
-  let kn = declare_constant id ~local (ParameterEntry pe, IsAssumption Conjectural) in
-  let () = assumption_message id in
+  let kn = declare_constant name ~local (ParameterEntry pe, IsAssumption Conjectural) in
+  let () = assumption_message name in
   Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
   (* This takes care of the implicits and hook for the current constant*)
   process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms;
@@ -494,7 +494,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
     let open Proof_global in
     let env = Global.env () in
     match proof with
-    | Some ({ id; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) ->
+    | Some ({ name; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
       let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -507,7 +507,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let ctx = UState.univ_entry ~poly universes in
       let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
       let sigma = Evd.from_env env in
-      finish_admitted env sigma id ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+      finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
     | None ->
       let pftree = Proof_global.get_proof lemma.proof in
       let scope = lemma.info.Info.scope in
@@ -537,7 +537,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let { Info.hook; impargs; other_thms } = lemma.info in
       let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
       let ctx = UState.check_univ_decl ~poly universes udecl in
-      finish_admitted env sigma name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
+      finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -547,15 +547,15 @@ let finish_proved env sigma opaque idopt po info =
   let open Proof_global in
   let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
   match po with
-  | { id; entries=[const]; universes; udecl; poly } ->
+  | { name; entries=[const]; universes; udecl; poly } ->
     let is_opaque = match opaque with
       | Transparent -> false
       | Opaque      -> true
     in
     assert (is_opaque == const.proof_entry_opaque);
-    let id = match idopt with
-      | None -> id
-      | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+    let name = match idopt with
+      | None -> name
+      | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Future.fix_exn_of const.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
@@ -565,14 +565,14 @@ let finish_proved env sigma opaque idopt po info =
       let r = match scope with
         | Discharge ->
           let c = SectionLocalDef const in
-          let _ = declare_variable id (Lib.cwd(), c, k) in
+          let _ = declare_variable name (Lib.cwd(), c, k) in
           let () = if should_suggest
-            then Proof_using.suggest_variable (Global.env ()) id
+            then Proof_using.suggest_variable (Global.env ()) name
           in
-          VarRef id
+          VarRef name
         | Global local ->
           let kn =
-            declare_constant id ~local (DefinitionEntry const, k) in
+            declare_constant name ~local (DefinitionEntry const, k) in
           let () = if should_suggest
             then Proof_using.suggest_constant (Global.env ()) kn
           in
@@ -580,7 +580,7 @@ let finish_proved env sigma opaque idopt po info =
           Declare.declare_univ_binders gr (UState.universe_binders universes);
           gr
       in
-      definition_message id;
+      definition_message name;
       (* This takes care of the implicits and hook for the current constant*)
       process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
     with e when CErrors.noncritical e ->