Adding a bit of documentation in the mli.

10 files changed, 27 insertions, 10 deletions

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ffff2c5dd..111d0f3e8 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -11,7 +11,7 @@ open Term
 open Evd
 open Environ
 
-(** {5 This modules provides useful functions for unification modulo evars } *)
+(** This module provides useful higher-level functions for evar manipulation. *)
 
 (** {6 Metas} *)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 3ae6e586c..df491c27b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -12,7 +12,10 @@ open Names
 open Term
 open Environ
 
-(** {5 Existential variables and unification states}
+(** This file defines the pervasive unification state used everywhere in Coq
+    tactic engine. It is very low-level and most of the functions exported here
+    are irrelevant to the standard API user. Consider using {!Evarutil},
+    {!Sigma} or {!Proofview} instead.
 
     A unification state (of type [evar_map]) is primarily a finite mapping
     from existential variables to records containing the type of the evar
@@ -23,6 +26,8 @@ open Environ
     It also contains conversion constraints, debugging information and
     information about meta variables. *)
 
+(** {5 Existential variables and unification states} *)
+
 (** {6 Evars} *)
 
 type evar = existential_key
@@ -343,7 +348,6 @@ val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b
 module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
 module Monad  : Monad.S with type +'a t = evar_map -> 'a * evar_map
 
-
 (** {5 Meta machinery}
 
     These functions are almost deprecated. They were used before the
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 19041f169..5db373199 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -8,7 +8,9 @@
 
 open Proofview.Notations
 
-(** Potentially focussing tactics *)
+(** This module defines potentially focussing tactics. They are used by Ltac to
+    emulate the historical behaviour of always-focussed tactics while still
+    allowing to remain global when the goal is not needed. *)
 
 type +'a focus
 
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 42e1e3784..b70671a2d 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Interpretation functions for generic arguments. *)
+(** Interpretation functions for generic arguments and interpreted Ltac
+    values. *)
 
 open Names
 open Genarg
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index c5160443b..dd122cca0 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This file defines the low-level monadic operations used by the
+(** This file implements the low-level monadic operations used by the
     tactic monad. The monad is divided into two layers: a non-logical
     layer which consists in operations which will not (or cannot) be
     backtracked in case of failure (input/output or persistent state)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index a2923fee9..e5c156b4e 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This file features facilities to generate fresh names. *)
+
 open Names
 open Term
 open Environ
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 0aff0a720..637414cce 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -7,7 +7,8 @@
 (************************************************************************)
 
 (** This file defines the datatypes used as internal states by the
-    tactic monad, and specialises the [Logic_monad] to these type. *)
+    tactic monad, and specialises the [Logic_monad] to these types. It should
+    not be used directly. Consider using {!Proofview} instead. *)
 
 (** {6 Traces} *)
 
diff --git a/engine/sigma.mli b/engine/sigma.mli
index 643bea403..aaf603efd 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -12,7 +12,9 @@ open Constr
 (** Monotonous state enforced by typing.
 
     This module allows to constrain uses of evarmaps in a monotonous fashion,
-    and in particular statically suppress evar leaks and the like.
+    and in particular statically suppress evar leaks and the like. To this
+    ends, it defines a type of indexed evarmaps whose phantom typing ensures
+    monotonous use.
 *)
 
 (** {5 Stages} *)
@@ -32,7 +34,7 @@ val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
 (** {5 Monotonous evarmaps} *)
 
 type 'r t
-(** Stage-indexed evarmaps.  *)
+(** Stage-indexed evarmaps. This is just a plain evarmap with a phantom type. *)
 
 type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
 (** Return values at a later stage *)
diff --git a/engine/termops.mli b/engine/termops.mli
index c2a4f3323..76a31037b 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This file defines various utilities for term manipulation that are not
+    needed in the kernel. *)
+
 open Pp
 open Names
 open Term
diff --git a/engine/uState.mli b/engine/uState.mli
index c5c454020..0cdc6277a 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Universe unification states *)
+(** This file defines universe unification states which are part of evarmaps.
+    Most of the API below is reexported in {!Evd}. Consider using higher-level
+    primitives when needed. *)
 
 open Names