Adding a bit of documentation in the mli.

10 files changed, 26 insertions, 26 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 59b166ea0..e9236b1da 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This file defines clausenv, which is a deprecated way to handle open terms
+    in the proof engine. Most of the API here is legacy except for the
+    evar-based clauses. *)
+
 open Names
 open Term
 open Environ
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 00e74a247..aa091aecd 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy components of the previous proof engine. *)
+
 open Term
 open Clenv
 open Tacexpr
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 8a3d6e815..6a79c1f45 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This module implements the abstract interface to goals *)
+(** This module implements the abstract interface to goals. Most of the code
+    here is useless and should be eventually removed. Consider using
+    {!Proofview.Goal} instead. *)
 
 type goal = Evar.t
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 9aa4ac207..2764d28c0 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy proof engine. Do not use in newly written code. *)
+
 open Names
 open Term
 open Evd
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index cfab8bd63..666730e1a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
+
 open Loc
 open Names
 open Term
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ef0d52b62..f7798a0ed 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy proof engine. Do not use in newly written code. *)
+
 open Evd
 open Names
 open Term
@@ -26,31 +28,6 @@ type prim_rule =
 
 type rule = prim_rule
 
-(** The type [goal sigma] is the type of subgoal. It has the following form
-{v   it    = \{ evar_concl = [the conclusion of the subgoal]
-             evar_hyps = [the hypotheses of the subgoal]
-             evar_body = Evar_Empty;
-             evar_info = \{ pgm    : [The Realizer pgm if any]
-                           lc     : [Set of evar num occurring in subgoal] \}\}
-   sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare]
-             ed : [A set of existential variables depending in the subgoal]
-               number of first evar,
-               it = \{ evar_concl = [the type of first evar]
-                      evar_hyps = [the context of the evar]
-                      evar_body = [the body of the Evar if any]
-                      evar_info = \{ pgm    : [Useless ??]
-                                    lc     : [Set of evars occurring
-                                              in the type of evar] \} \};
-               ...
-               number of last evar,
-               it = \{ evar_concl = [the type of evar]
-                      evar_hyps = [the context of the evar]
-                      evar_body = [the body of the Evar if any]
-                      evar_info = \{ pgm    : [Useless ??]
-                                    lc     : [Set of evars occurring
-                                              in the type of evar] \} \} \} v}
-*)
-
 type goal = Goal.goal
 
 type tactic = goal sigma -> goal list sigma
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index 1bf38b690..b2c65412f 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Utility code for section variables handling in Proof using... *)
+
 val process_expr :
   Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
     Names.Id.t list
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index b91911087..d4c2c4a6c 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
+
 open Names
 open Term
 open Pattern
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 17c7e28ca..a9798b704 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -6,6 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** The primitive refine tactic used to fill the holes in partial proofs. This
+    is the recommanded way to write tactics when the proof term is easy to
+    write down. Note that this is not the user-level refine tactic defined
+    in Ltac which is actually based on the one below. *)
+
 open Proofview
 
 (** {6 The refine tactic} *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index dd9153a02..6dcafb77a 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Legacy proof engine. Do not use in newly written code. *)
+
 open Evd
 open Proof_type