Cleanup of comments.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 32 insertions, 24 deletions

diff --git a/proofs/monads.ml b/proofs/monads.ml
index 9500c27893..ba14408641 100644
--- a/proofs/monads.ml
+++ b/proofs/monads.ml
@@ -144,9 +144,16 @@ end
    The paper also contains the rational for the [split] abstraction.
 
    An explanation of how to derive such a monad from mathematical
-   principle can be found in "Kan Extensions for Program Optimisation" by
-   Ralf Hinze. *)
-(* arnaud: ajouter commentaire sur la vision "liste" *)
+   principles can be found in "Kan Extensions for Program
+   Optimisation" by Ralf Hinze.
+
+   One way to think of the [Logic] functor is to imagine ['a
+   Logic(X).t] to represent list of ['a] with an exception at the
+   bottom (leaving the monad-transforming issues aside, as they don't
+   really work well with lists). Each of the element is a valid
+   result, sequentialising with a [f:'a -> 'b t] is done by applying
+   [f] to each element and then flatten the list, [plus] is
+   concatenation, and [split] is pattern-matching. *)
 (* spiwack: I added the primitives from [IO] directly in the [Logic]
    signature for convenience. It doesn't really make sense, strictly
    speaking, as they are somewhat deconnected from the semantics of
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 406de8d2b2..3f80da785c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -270,23 +270,27 @@ let tclFOCUS i j t env =
        of course I haven't made them algebraic yet. *)
     tclZERO e env
 
-(* arnaud: vérifier les commentaires de dispatch vis-à-vis de l'ordre
-   d'évaluation des buts. Ne pas oublier le mli *)
-(* arnaud: commenter [tclDISPATCHL] *)
 (* 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]. *)
+   [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. *)
 exception SizeMismatch
 let _ = Errors.register_handler begin function
   | SizeMismatch -> Errors.error "Incorrect number of goals."
   | _ -> raise Errors.Unhandled
 end
 (* spiwack: we use an parametrised function to generate the dispatch tacticals.
-    [tclDISPATCHGEN] takes a [null] argument to generate the return value
-    if there are no goal under focus, and a [join] argument to explain how
-    the return value at two given lists of subgoals are combined when
-    both lists are being concatenated.
-    [join] and [null] need be some sort of comutative monoid. *)
+   [tclDISPATCHGEN] takes a [null] argument to generate the return value
+   if there are no goal under focus, and a [join] argument to explain how
+   the return value at two given lists of subgoals are combined when
+   both lists are being concatenated.
+   [join] and [null] need be some sort of comutative monoid. *)
 
 let rec tclDISPATCHGEN null join tacs env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -366,9 +370,6 @@ let sensitive_on_proofview s env step =
   with e when Errors.noncritical e ->
     tclZERO e env
 
-(* arnaud: on pourrait regarder la liste de buts aussi, mais je
-   ne sais pas encore comment. Pour l'instant on fait au plus
-   simple. *)
 let tclPROGRESS t env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 2a69ccaf3f..d2db5be9a3 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -158,14 +158,15 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tact
 val tclFOCUS : int -> int -> 'a tactic -> 'a 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].
-    [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
-    and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
-    corresponds to that of the tactic which created [g].
-    It is to be noted that the return value of [tclDISPATCHS ts] makes only
-    sense in the goals immediatly built by it, and would cause an anomaly
-    is used otherwise. *)
+   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. *)
 val tclDISPATCH : unit tactic list -> unit tactic
 val tclDISPATCHL : 'a tactic list -> 'a list tactic
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 42aa0cfb51..3c3bb3970f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -66,7 +66,6 @@ exception FailError of int * std_ppcmds Lazy.t
 (* The Fail tactic *)
 let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
 
-(* arnaud: pas utilisée supprimer ? *)
 let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =