Cleanup of comments.

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

8 files changed, 33 insertions, 34 deletions

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a4f8641ddb..a3a2b25e44 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-(* arnaud: veiller à l'aspect tutorial des commentaires *)
-
 open Compat
 open Pp
 open Tok
@@ -36,7 +34,7 @@ let pr_goal gs =
 		       str "============================" ++ fnl ()  ++
 		       thesis ++ str " " ++  pc) ++ fnl ()
 
-(* arnaud: rebrancher ça 
+(* arnaud: rebrancher ça ?
 let pr_open_subgoals () =
   let p = Proof_global.give_me_the_proof () in
   let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
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 =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fd6dd03613..35b0dc7ff8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1105,7 +1105,6 @@ si après Intros la conclusion matche le pattern.
 
 let (forward_interp_tactic, extern_interp) = Hook.make ()
 
-(* arnaud: potentiel bug avec ce try/with *)
 let conclPattern concl pat tac =
   let constr_bindings =
     match pat with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a7b04bee24..babc889446 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1550,9 +1550,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
 (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
    it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
 
-(* arnaud: il va y avoir un bug là-dedans. Le try ne se déclenche pas
-   au bon endroit. Il faut convertir test en une Proofview.tactic
-   pour la gestion des exceptions. *)
 let subst_one_var dep_proof_ok x =
   Proofview.Goal.hyps >>= fun hyps ->
   let hyps = Environ.named_context_of_val hyps in
@@ -1593,7 +1590,6 @@ let default_subst_tactic_flags () =
   else
     { only_leibniz = true; rewrite_dependent_proof = false }
 
-(* arnaud: encore des erreurs potentiels avec ces try/with *)
 let subst_all ?(flags=default_subst_tactic_flags ()) =
   Tacmach.New.of_old find_eq_data_decompose >>= fun find_eq_data_decompose ->
   let test (_,c) =
@@ -1639,7 +1635,6 @@ let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t)
 let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t)
 let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t)
 
-(* arnaud: toujours des histoires de try/with *)
 let rewrite_multi_assumption_cond cond_eq_term cl =
   let rec arec = function
     | [] -> error "No such assumption."
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 233e9f85b3..5b1ae69e33 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -869,7 +869,6 @@ let find_eliminator c gl =
   let c = lookup_eliminator ind (elimination_sort_of_goal gl) in
   {elimindex = None; elimbody = (c,NoBindings)}
 
-(* arnaud: probable bug avec le try *)
 let default_elim with_evars (c,_ as cx) =
   Proofview.tclORELSE
     (Tacmach.New.of_old (find_eliminator c) >>= fun elim ->