Proofview: documentation and re-ordering.

1 files changed, 289 insertions, 214 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 914af982d6..3529c3c1bb 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -6,26 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* The proofview datastructure is a pure datastructure underlying the notion
-   of proof (namely, a proof is a proofview which can evolve and has safety
-   mechanisms attached).
-   The general idea of the structure is that it is composed of a chemical
-   solution: an unstructured bag of stuff which has some relations with
-   one another, which represents the various subnodes of the proof. Together
-   with a comb: a datastructure that gives some order to some of these nodes,
-   namely the (focused) open goals.
-   The natural candidate for the solution is an {!Evd.evar_map}, that is
-   a calculus of evars. The comb is then a list of goals (evars wrapped
-   with some extra information, like possible name anotations).
-   There is also need of a list of the evars which initialised the proofview
-   to be able to return information about the proofview. *)
+(** This files defines the basic mechanism of proofs: the [proofview]
+    type is the state which tactics manipulate (a global state for
+    existential variables, together with the list of goals), and the type
+    ['a tactic] is the (abstract) type of tactics modifying the proof
+    state and returning a value of type ['a]. *)
 
 open Term
 
+(** Main state of tactics *)
 type proofview
 
-(* Returns a stylised view of a proofview for use by, for instance,
-   ide-s. *)
+(** Returns a stylised view of a proofview for use by, for instance,
+    ide-s. *)
 (* spiwack: the type of [proofview] will change as we push more
    refined functions to ide-s. This would be better than spawning a
    new nearly identical function everytime. Hence the generic name. *)
@@ -33,243 +26,272 @@ type proofview
    the [evar_map] context. *)
 val proofview : proofview -> Goal.goal list * Evd.evar_map
 
+
+(** {6 Starting and querying a proof view} *)
+
+(** Abstract representation of the initial goals of a proof. *)
 type entry
 
-(* Initialises a proofview, the argument is a list of environement, 
-   conclusion types, creating that many initial goals. *)
+(** Initialises a proofview, the main argument is a list of
+    environements (including a [named_context] which are used as
+    hypotheses) pair with conclusion types, creating accordingly many
+    initial goals. Because a proof does not necessarily starts in an
+    empty [evar_map] (indeed a proof can be triggered by an incomplete
+    pretyping), [init] takes an additional argument to represent the
+    initial [evar_map]. *)
 val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
 
+(** A [telescope] is a list of environment and conclusion like in
+    {!init}, except that each element may depend on the previous
+    goals. The telescope passes the goals in the form of a
+    [Term.constr] which represents the goal as an [evar]. The
+    [evar_map] is threaded in state passing style. *)
 type telescope =
   | TNil of Evd.evar_map
   | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
 
-(* Like [init], but goals are allowed to be depedenent on one
-   another. Dependencies between goals is represented with the type
-   [telescope] instead of [list]. *)
+(** Like {!init}, but goals are allowed to be dependent on one
+    another. Dependencies between goals is represented with the type
+    [telescope] instead of [list]. Note that the first [evar_map] of
+    the telescope plays the role of the [evar_map] argument in
+    [init]. *)
 val dependent_init  : telescope -> entry * proofview
 
-(* Returns whether this proofview is finished or not. That is,
-   if it has empty subgoals in the comb. There could still be unsolved
-   subgoaled, but they would then be out of the view, focused out. *)
+(** [finished pv] is [true] if and only if [pv] is complete. That is,
+    if it has an empty list of focused goals. There could still be
+    unsolved subgoaled, but they would then be out of focus. *)
 val finished : proofview -> bool
 
-(* Returns the current value of the proofview partial proofs. *)
+(** Returns the current [evar] state. *)
 val return : proofview -> Evd.evar_map
 
 val partial_proof : entry -> proofview -> constr list
 val initial_goals : entry -> (constr * types) list
 
-(*** Focusing operations ***)
 
-(* Type of the object which allow to unfocus a view.*)
+
+(** {6 Focusing commands} *)
+
+(** A [focus_context] represents the part of the proof view which has
+    been removed by a focusing action, it can be used to unfocus later
+    on. *)
 type focus_context
 
-(* Returns a stylised view of a focus_context for use by, for
-   instance, ide-s. *)
+(** Returns a stylised view of a focus_context for use by, for
+    instance, ide-s. *)
 (* spiwack: the type of [focus_context] will change as we push more
    refined functions to ide-s. This would be better than spawning a
    new nearly identical function everytime. Hence the generic name. *)
-(* In this version: returns the number of goals that are held *)
+(* In this version: the goals in the context, as a "zipper" (the first
+   list is in reversed order). *)
 val focus_context : focus_context -> Goal.goal list * Goal.goal list
 
-(* [focus i j] focuses a proofview on the goals from index [i] to index [j] 
-   (inclusive). (i.e. goals number [i] to [j] become the only goals of the
-   returned proofview).
-   It returns the focus proof, and a context for the focus trace. *)
+(** [focus i j] focuses a proofview on the goals from index [i] to
+    index [j] (inclusive, goals are indexed from [1]). I.e. goals
+    number [i] to [j] become the only focused goals of the returned
+    proofview.  It returns the focused proofview, and a context for
+    the focus stack. *)
 val focus : int -> int -> proofview -> proofview * focus_context
 
-(* Unfocuses a proofview with respect to a context. *)
+(** Unfocuses a proofview with respect to a context. *)
 val unfocus : focus_context -> proofview -> proofview
 
-(* The tactic monad:
-   - Tactics are objects which apply a transformation to all
-     the subgoals of the current view at the same time. By opposition
-     to the old vision of applying it to a single goal. It allows 
-     tactics such as [shelve_unifiable] or tactics to reorder
-     the focused goals (not done yet).
-     (* spiwack: the ordering of goals, though, is actually rather
-        brittle. It would be much more interesting to find a more
-        robust way to adress goals, I have no idea at this time 
-        though*) 
-     or global automation tactic for dependent subgoals (instantiating
-     an evar has influences on the other goals of the proof in progress,
-     not being able to take that into account causes the current eauto
-     tactic to fail on some instances where it could succeed).
-     Another benefit is that it is possible to write tactics that can
-     be executed even if there are no focused goals.
-   - Tactics form a monad ['a tactic], in a sense a tactic can be 
-     seens as a function (without argument) which returns a value
-     of type 'a and modifies the environement (in our case: the view).
-     Tactics of course have arguments, but these are given at the 
-     meta-level as OCaml functions.
-     Most tactics in the sense we are used to return [()], that is
-     no really interesting values. But some might pass information 
-     around.
-     (* spiwack: as far as I'm aware this doesn't really relate to
-        F. Kirchner and C. Muñoz.
-     *)
-     The tactics seen in Coq's Ltac are (for now at least) only 
-     [unit tactic], the return values are kept for the OCaml toolkit.
-     The operation or the monad are [Proofview.tclUNIT] (which is the 
-     "return" of the tactic monad) [Proofview.tclBIND] (which is
-     the "bind") and [Proofview.tclTHEN] (which is a specialized
-     bind on unit-returning tactics).
+
+(** {6 The tactic monad} *)
+
+(** - Tactics are objects which apply a transformation to all the
+    subgoals of the current view at the same time. By opposition to
+    the old vision of applying it to a single goal. It allows tactics
+    such as [shelve_unifiable], tactics to reorder the focused goals,
+    or global automation tactic for dependent subgoals (instantiating
+    an evar has influences on the other goals of the proof in
+    progress, not being able to take that into account causes the
+    current eauto tactic to fail on some instances where it could
+    succeed).  Another benefit is that it is possible to write tactics
+    that can be executed even if there are no focused goals.
+    - Tactics form a monad ['a tactic], in a sense a tactic can be
+    seens as a function (without argument) which returns a value of
+    type 'a and modifies the environement (in our case: the view).
+    Tactics of course have arguments, but these are given at the
+    meta-level as OCaml functions.  Most tactics in the sense we are
+    used to return [()], that is no really interesting values. But
+    some might pass information around.  The tactics seen in Coq's
+    Ltac are (for now at least) only [unit tactic], the return values
+    are kept for the OCaml toolkit.  The operation or the monad are
+    [Proofview.tclUNIT] (which is the "return" of the tactic monad)
+    [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN]
+    (which is a specialized bind on unit-returning tactics).
+    - Tactics have support for full-backtracking. Tactics can be seen
+    having multiple success: if after returning the first success a
+    failure is encountered, the tactic can backtrack and use a second
+    success if available. The state is backtracked to its previous
+    value, except the non-logical state defined in the {!NonLogical}
+    module below.
 *)
 
 
+(** The abstract type of tactics *)
 type +'a tactic 
 
-type 'a case =
-| Fail of exn
-| Next of 'a * (exn -> 'a tactic)
-
-(* Applies a tactic to the current proofview. *)
-(* the return boolean signals the use of an unsafe tactic, in which
-   case it is [false]. *)
+(** Applies a tactic to the current proofview. Returns a tuple
+    [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv]
+    is the updated proofview, [b] a boolean which is [true] if the
+    tactic has not done any action considered unsafe (such as
+    admitting a lemma), [sh] is the list of goals which have been
+    shelved by the tactic, and [gu] the list of goals on which the
+    tactic has given up. In case of multiple success the first one is
+    selected. If there is no success, fails with
+    {!Logic_monad.TacticFailure}*)
 val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                    * proofview
                                                    * (bool*Goal.goal list*Goal.goal list)
 
-(*** tacticals ***)
+(** {7 Monadic primitives} *)
 
-(* Unit of the tactic monad *)
+(** Unit of the tactic monad. *)
 val tclUNIT : 'a -> 'a tactic
  
-(* Bind operation of the tactic monad *)
+(** Bind operation of the tactic monad. *)
 val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
 
-(* Interprets the ";" (semicolon) of Ltac.
-   As a monadic operation, it's a specialized "bind"
-   on unit-returning tactic (meaning "there is no value to bind") *)
+(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
+    it's a specialized "bind". *)
 val tclTHEN : unit tactic -> 'a tactic -> 'a tactic
 
-(* [tclIGNORE t] has the same operational content as [t],
-   but drops the value at the end. *)
+(** [tclIGNORE t] has the same operational content as [t], but drops
+    the returned value. *)
 val tclIGNORE : 'a tactic -> unit tactic
 
-(* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
-   of [t1] have been depleted and it failed with [e], then it behaves
-   as [t2 e].  No interleaving at this point. *)
-val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
+(** Generic monadic combinators for tactics. *)
+module Monad : Monad.S with type +'a t = 'a tactic
+
+(** {7 Failure and backtracking} *)
 
-(* [tclZERO] always fails *)
+(** [tclZERO e] fails with exception [e]. It has no success. *)
 val tclZERO : exn -> 'a tactic
 
-(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
-   or [t2 e] if [t1] fails with [e]. *)
-val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
+(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
+    the successes of [t1] have been depleted and it failed with [e],
+    then it behaves as [t2 e]. In other words, [tclOR] inserts a
+    backtracking point. *)
+val tclOR : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
 
-(* [tclCASE t] observes the head of the tactic and returns it as a value *)
-val tclCASE : 'a tactic -> 'a case tactic
+(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
+    success or [t2 e] if [t1] fails with [e]. It is analogous to
+    [try/with] handler of exception in that it is not a backtracking
+    point. *)
+val tclORELSE : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
 
-(* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
-   succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
-   fails with [e], then it behaves as [f e]. *)
+(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
+    succeeds at least once then it behaves as [tclBIND a s] otherwise,
+    if [a] fails with [e], then it behaves as [f e]. *)
 val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tactic
 
-(* [tclONCE t] fails if [t] fails, otherwise it has exactly one
-   success. *)
+(** [tclONCE t] behave like [t] except it has at most one success:
+    [tclONCE t] stops after the first success of [t]. If [t] fails
+    with [e], [tclONCE t] also fails with [e]. *)
 val tclONCE : 'a tactic -> 'a tactic
 
-(* [tclBREAK f t] is a generalization of [tclONCE t]. Instead of stopping at the
-  first element encountered, it waits for the tactic to return an exception
-  satisfying [f], and drop the remaining results. [tclONCE t] is equivalent to
-  [tclBREAK (fun _ -> true) t]. *)
+(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
+    success. Otherwise it fails. The tactic [t] is run until its first
+    success, then a failure with exception [e] is simulated. It [t]
+    yields another success, then [tclEXACTLY_ONCE e t] fails with
+    [MoreThanOneSuccess] (it is a user error). Otherwise,
+    [tclEXACTLY_ONCE e t] succeeds with the first success of
+    [t]. Notice that the choice of [e] is relevant, as the presence of
+    further successes may depend on [e] (see {!tclOR}). *)
+exception MoreThanOneSuccess
+val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
+
+(** [tclCASE t] splits [t] into its first success and a
+    continuation. It is the most general primitive to control
+    backtracking. *)
+type 'a case =
+  | Fail of exn
+  | Next of 'a * (exn -> 'a tactic)
+val tclCASE : 'a tactic -> 'a case tactic
+
+(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
+    stopping after the first success, it succeeds like [t] until a
+    failure with an exception [e] such that [p e=true] is raised. At
+    which point it drop the remaining successes. [tclONCE t] is
+    equivalent to [tclBREAK (fun _ -> true) t]. *)
 val tclBREAK : (exn -> bool) -> 'a tactic -> 'a tactic
 
-(* [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
-   success. Otherwise it fails.  It may behave differently than [t] as
-   there may be extra non-logical effects used to discover that [t]
-   does not have a second success. Moreover the second success may be
-   conditional on the error received: [e] is used. *)
-val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
 
-(* Focuses a tactic at a range of subgoals, found by their indices.
-   The other goals are restored to the focus when the tactic is done.
+(** {7 Focusing tactics} *)
 
-   If the specified range doesn't correspond to existing goals, fails
-   with [NoSuchGoals]. *)
+(** [tclFOCUS i j t] applies [t] after focusing on the goals number
+    [i] to [j] (see {!focus}). The rest of the goals is restored after
+    the tactic action. If the specified range doesn't correspond to
+    existing goals, fails with [NoSuchGoals] (a user error). *)
 exception NoSuchGoals of int
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
+(** [tclFOCUSID x t] applies [t] on a (single) focused goal like
+    {!tclFOCUS}. The goal is found by its name rather than its
+    number.*)
 val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
 
-(* Focuses a tactic at a range of subgoals, found by their indices.
-   The other goals are restored to the focus when the tactic is done.
-
-   If the specified range doesn't correspond to existing goals, behaves
-   like [tclUNIT ()]. *)
+(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the
+    specified range doesn't correspond to existing goals, behaves like
+    [tclUNIT ()] instead of failing. *)
 val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic
 
-(* Dispatch tacticals are used to apply a different tactic to each goal under
-   consideration. They come in two flavours:
-   [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
-   [tclDISPATCHL] takes a list of ['a tactic] and returns an ['a list tactic].
 
-   They both work by applying each of the tactic to the corresponding
-   goal (starting with the first goal). In the case of [tclDISPATCHL],
-   the tactic returns a list of the same size as the argument list (of
-   tactics), each element being the result of the tactic executed in
-   the corresponding goal.
+(** {7 Dispatching on goals} *)
+
+(** Dispatch tacticals are used to apply a different tactic to each
+    goal under focus. They come in two flavours: [tclDISPATCH] takes a
+    list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL]
+    takes a list of ['a tactic] and returns an ['a list tactic].
 
-   When the length of the tactic list is not the number of goal,
-   raises [SizeMismatch (g,t)] where [g] is the number of available
-   goals, and [t] the number of tactics passed. *)
+    They both work by applying each of the tactic in a focus
+    restricted to the corresponding goal (starting with the first
+    goal). In the case of [tclDISPATCHL], the tactic returns a list of
+    the same size as the argument list (of tactics), each element
+    being the result of the tactic executed in the corresponding goal.
+
+    When the length of the tactic list is not the number of goal,
+    raises [SizeMismatch (g,t)] where [g] is the number of available
+    goals, and [t] the number of tactics passed. *)
 exception SizeMismatch of int*int
 val tclDISPATCH : unit tactic list -> unit tactic
 val tclDISPATCHL : 'a tactic list -> 'a list tactic
 
-(* [tclEXTEND b r e] is a variant to [tclDISPATCH], where the [r] tactic
-    is "repeated" enough time such that every goal has a tactic assigned to it
-    ([b] is the list of tactics applied to the first goals, [e] to the last goals, and [r]
-    is applied to every goal in between. *)
+(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r]
+    tactic is "repeated" enough time such that every goal has a tactic
+    assigned to it ([b] is the list of tactics applied to the first
+    goals, [e] to the last goals, and [r] is applied to every goal in
+    between). *)
 val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
 
-(* [tclINDEPENDENT tac] runs [tac] on each goal successively, from the
-   first one to the last one. Backtracking in one goal is independent of
-   backtracking in another. *)
+(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from
+    the first one to the last one. Backtracking in one goal is
+    independent of backtracking in another. It is equivalent to
+    [tclEXTEND [] tac []]. *)
 val tclINDEPENDENT : unit tactic -> unit tactic
 
-(* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *)
-val tclPROGRESS : 'a tactic -> 'a tactic
-
-(* [tclEVARMAP] doesn't affect the proof, it returns the current evar_map. *)
-val tclEVARMAP : Evd.evar_map tactic
-
-(* [tclENV] doesn't affect the proof, it returns the current
-   environment.  It is not the environment of a particular goal,
-   rather the "global" environment of the proof. The goal-wise
-   environment is returned by {!Proofview.Goal.env}. *)
-val tclENV : Environ.env tactic
-
-(* [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Declareops.side_effects -> unit tactic
 
-(* Checks for interrupts *)
-val tclCHECKINTERRUPT : unit tactic
+(** {7 Goal manipulation} *)
 
-(* Shelves all the goals under focus. The goals are placed on the
-   shelf for later use (or being solved by side-effects). *)
+(** Shelves all the goals under focus. The goals are placed on the
+    shelf for later use (or being solved by side-effects). *)
 val shelve : unit tactic
 
-(* Shelves the unifiable goals under focus, i.e. the goals which
-   appear in other goals under focus (the unfocused goals are not
-   considered). *)
+(** Shelves the unifiable goals under focus, i.e. the goals which
+    appear in other goals under focus (the unfocused goals are not
+    considered). *)
 val shelve_unifiable : unit tactic
 
-(* This fails with error UnresolvedBindings if some goals are
-   dependent in the current list of goals under focus *)
-val check_no_dependencies : unit tactic
+(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
+    goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
+val guard_no_unifiable : unit tactic
 
-(* [unshelve l p] adds all the goals in [l] at the end of the focused
-   goals of p *)
+(** [unshelve l p] adds all the goals in [l] at the end of the focused
+    goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
-
-(* Gives up on the goal under focus. Reports an unsafe status. Proofs
-   with given up goals cannot be closed. *)
-val give_up : unit tactic
-
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
     is negative, then it puts the [n] last goals first.*)
 val cycle : int -> unit tactic
@@ -280,12 +302,49 @@ val cycle : int -> unit tactic
     [1] as well, rather than raising an error. *)
 val swap : int -> int -> unit tactic
 
-(** [revgoals] reverse the list of focused goals. *)
+(** [revgoals] reverses the list of focused goals. *)
 val revgoals : unit tactic
 
 (** [numgoals] returns the number of goals under focus. *)
 val numgoals : int tactic
 
+
+(** {7 Access primitives} *)
+
+(** [tclEVARMAP] doesn't affect the proof, it returns the current
+    [evar_map]. *)
+val tclEVARMAP : Evd.evar_map tactic
+
+(** [tclENV] doesn't affect the proof, it returns the current
+    environment. It is not the environment of a particular goal,
+    rather the "global" environment of the proof. The goal-wise
+    environment is obtained via {!Proofview.Goal.env}. *)
+val tclENV : Environ.env tactic
+
+
+(** {7 Put-like primitives} *)
+
+(** [tclEFFECTS eff] add the effects [eff] to the current state. *)
+val tclEFFECTS : Declareops.side_effects -> unit tactic
+
+(** [mark_as_unsafe] declares the current tactic is unsafe. *)
+val mark_as_unsafe : unit tactic
+
+(** Gives up on the goal under focus. Reports an unsafe status. Proofs
+    with given up goals cannot be closed. *)
+val give_up : unit tactic
+
+
+(** {7 Control primitives} *)
+
+(** [tclPROGRESS t] checks the state of the proof after [t]. It it is
+    identical to the state before, then [tclePROGRESS t] fails, otherwise
+    it succeeds like [t]. *)
+val tclPROGRESS : 'a tactic -> 'a tactic
+
+(** Checks for interrupts *)
+val tclCHECKINTERRUPT : unit tactic
+
 exception Timeout
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
@@ -295,48 +354,51 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
     identifying annotation if present *)
 val tclTIME : string option -> 'a tactic -> 'a tactic
 
-(** [mark_as_unsafe] signals that the current tactic is unsafe. *)
-val mark_as_unsafe : unit tactic
+(** {7 Unsafe primitives} *)
 
+(** The primitives in the [Unsafe] module should be avoided as much as
+    possible, since they can make the proof state inconsistent. They are
+    nevertheless helpful, in particular when interfacing the pretyping and
+    the proof engine. *)
 module Unsafe : sig
 
-  (* Assumes the new evar_map does not change existing goals *)
+  (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If
+      [sigma] has new unresolved [evar]-s they will not appear as
+      goal. If goals have been solved in [sigma] they will still
+      appear as unsolved goals. *)
   val tclEVARS : Evd.evar_map -> unit tactic
-
-  (* [tclNEWGOALS gls] adds the goals [gls] to the ones currently
-     being proved, appending them to the list of focussed goals. If a
-     goal is already solved, it is not added. Prefer the other
-     primitives when possible. *)
-  val tclNEWGOALS : Goal.goal list -> unit tactic
-
     
-  (* Assumes the new evar_map might be solving some existing goals *)
+  (** Like {!tclEVARS} but also checks whether goals have been solved. *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
-  (* Set the evar universe context *)
+  (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
+      being proved, appending them to the list of focused goals. If a
+      goal is already solved, it is not added. *)
+  val tclNEWGOALS : Goal.goal list -> unit tactic
+
+  (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
 
-  (* Clears the future goals store in the proof. *)
+  (** Clears the future goals store in the proof view. *)
   val reset_future_goals : proofview -> proofview
 end
 
-module Monad : Monad.S with type +'a t = 'a tactic
+(** {7 Notations} *)
 
-(* Notations for building tactics. *)
 module Notations : sig
 
-  (* tclBIND *)
+  (** {!tclBIND} *)
   val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-  (* tclTHEN *)
+  (** {!tclTHEN} *)
   val (<*>) : unit tactic -> 'a tactic -> 'a tactic
-  (* tclOR *)
+  (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
+
 end
 
 
-(* The module goal provides an interface for goal-dependent tactics. *)
-(* spiwack: there are still parts of the code which depend on proofs/goal.ml.
-   Eventually I'll try to remove it in favour of [Proofview.Goal] *)
+(** {6 Goal-dependent tactics} *)
+
 module Goal : sig
 
   (** The type of goals. The parameter type is a phantom argument indicating
@@ -352,65 +414,78 @@ module Goal : sig
   (** Normalises the argument goal. *)
   val normalize : 'a t -> [ `NF ] t tactic
 
-  (* [concl], [hyps], [env] and [sigma] given a goal [gl] return
-     respectively the conclusion of [gl], the hypotheses of [gl], the
-     environment of [gl] (i.e. the global environment and the hypotheses)
-     and the current evar map. *)
+  (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
+      respectively the conclusion of [gl], the hypotheses of [gl], the
+      environment of [gl] (i.e. the global environment and the
+      hypotheses) and the current evar map. *)
   val concl : [ `NF ] t -> Term.constr
   val hyps : [ `NF ] t -> Context.named_context
   val env : 'a t -> Environ.env
   val sigma : 'a t -> Evd.evar_map
 
+  (** Returns the goal's conclusion even if the goal is not
+      normalised. *)
   val raw_concl : 'a t -> Term.constr
 
-  (* [nf_enter t] execute the goal-dependent tactic [t] in each goal
-     independently. In particular [t] need not backtrack the same way in
-     each goal. *)
+  (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
+      independently, in the manner of {!tclINDEPENDENT} except that
+      the current goal is also given as an argument to [t]. The goal
+      is normalised with respect to evars. *)
   val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
 
-  (** Same as nf_enter, but does not normalize the goal beforehand. *)
+  (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t tactic list tactic
 
-  (* compatibility: avoid if possible *)
+  (** Compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Evar.t
 
 end
 
-(** A light interface for building tactics out of partial term. Be careful,
-    the [refine] function does not do any typechecking, so you may construct
-    ill-typed terms without noticing. *)
+
+(** {6 The refine tactic} *)
+
 module Refine : sig
 
+  (** {7 Refinement primitives} *)
+
+  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
+  (** In [refine ?unsafe t], [t] is a term with holes under some
+      [evar_map] context. The term [t] is used as a partial solution
+      for the current goal (refine is a goal-dependent tactic), the
+      new holes created by [t] become the new subgoals. Exception
+      raised during the interpretation of [t] are caught and result in
+      tactic failures. If [unsafe] is [true] (default) [t] is
+      type-checked beforehand. *)
+
+  (** {7 Helper functions} *)
+
   val with_type : Environ.env -> Evd.evar_map ->
     Term.constr -> Term.types -> Evd.evar_map * Term.constr
   (** [with_type env sigma c t] ensures that [c] is of type [t]
       inserting a coercion if needed. *)
 
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
-  (** Given a term with holes that have been generated through
-      {!new_evar}, this function fills the current hole with the given
-      constr and creates goals for all the holes in their generation
-      order. The [evar_map] in the argument function is assumed to
-      only increase. Exceptions raised by the function are caught. *)
-
-  val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
-(** Like {!refine} except the refined term is coerced to the conclusion of the
-    current goal. *)
+  val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic
+  (** Like {!refine} except the refined term is coerced to the conclusion of the
+      current goal. *)
 
 end
 
-(* The [NonLogical] module allows the execution of side effects in tactics
-   (non-logical side-effects are not discarded at failures). *)
+
+(** {6 Non-logical state} *)
+
+(** The [NonLogical] module allows the execution of effects (including
+    I/O) in tactics (non-logical side-effects are not discarded at
+    failures). *)
 module NonLogical : module type of Logic_monad.NonLogical
 
-(* [tclLIFT c] includes the non-logical command [c] in a tactic. *)
+(** [tclLIFT c] is a tactic which behaves exactly as [c]. *)
 val tclLIFT : 'a NonLogical.t -> 'a tactic
 
 
-
+(**/**)
 
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 : sig