[proof] API Documentation fixes.

2 files changed, 15 insertions, 11 deletions

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