Fixing spelling: pr_coma -> pr_comma

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

4 files changed, 12 insertions, 12 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index cf5a58eea4..2d63b20bb5 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -164,7 +164,7 @@ let pr_evar pr n l =
    | Some l ->
        spc () ++ pr_in_comment
          (fun l ->
-	   str"[" ++ hov 0 (prlist_with_sep pr_coma (pr ltop) l) ++ str"]")
+	   str"[" ++ hov 0 (prlist_with_sep pr_comma (pr ltop) l) ++ str"]")
          (List.rev l)
    | None -> mt()))
 
@@ -657,11 +657,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
   | Unfold l ->
       hov 1 (str "unfold" ++ spc() ++
-             prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l)
+             prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
   | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l ->
       hov 1 (str "pattern" ++
-        pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
+        pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l)
 
   | Red true -> error "Shouldn't be accessible from user."
   | ExtraRedExpr s -> str s
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9714b7fa95..f410e38f3f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -490,14 +490,14 @@ let pr_match_rule m pr pr_pat = function
       spc () ++ str "=>" ++ brk (1,4) ++ pr t
 (*
   | Pat (rl,mp,t) ->
-      hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl ++
+      hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl ++
         (if rl <> [] then spc () else mt ()) ++
          hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
 	 str "=>" ++ brk (1,4) ++ pr t))
 *)
   | Pat (rl,mp,t) ->
       hov 0 (
-	hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl) ++
+	hv 0 (prlist_with_sep pr_comma (pr_match_hyps pr_pat) rl) ++
         (if rl <> [] then spc () else mt ()) ++
         hov 0 (
 	  str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
@@ -544,7 +544,7 @@ let pr_hintbases = function
 let pr_auto_using prc = function
   | [] -> mt ()
   | l -> spc () ++
-      hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_coma prc l)
+      hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
 let pr_autoarg_adding = function
   | [] -> mt ()
@@ -703,7 +703,7 @@ and pr_atom1 = function
   | TacApply (a,ev,cb,inhyp) ->
       hov 1 ((if a then mt() else str "simple ") ++
              str (with_evars ev "apply") ++ spc () ++
-             prlist_with_sep pr_coma pr_with_bindings cb ++
+             prlist_with_sep pr_comma pr_with_bindings cb ++
              pr_in_hyp_as pr_ident inhyp)
   | TacElim (ev,cb,cbo) ->
       hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++
@@ -732,7 +732,7 @@ and pr_atom1 = function
              pr_assertion pr_lconstr pr_constr ipat c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
-             prlist_with_sep pr_coma (fun (cl,na) ->
+             prlist_with_sep pr_comma (fun (cl,na) ->
 	       pr_with_occurrences pr_constr cl ++ pr_as_name na)
 	     l)
   | TacGeneralizeDep c ->
@@ -762,7 +762,7 @@ and pr_atom1 = function
   | TacInductionDestruct (isrec,ev,(l,cl)) ->
       hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
              spc () ++
-             prlist_with_sep pr_coma (fun (h,e,ids) ->
+             prlist_with_sep pr_comma (fun (h,e,ids) ->
 	       prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
 	       pr_with_induction_names ids ++
                pr_opt pr_eliminator e) l ++
@@ -826,7 +826,7 @@ and pr_atom1 = function
   (* Constructors *)
   | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l)
   | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l)
-  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_coma pr_bindings l)
+  | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_comma pr_bindings l)
   | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l)
   | TacAnyConstructor (ev,Some t) ->
       hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 882a94ffbb..cc04f8f345 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -69,7 +69,7 @@ let print_impl_args_by_name max = function
   | []  -> mt ()
   | impls ->
       hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++
-      prlist_with_sep pr_coma pr_implicit impls ++ spc() ++
+      prlist_with_sep pr_comma pr_implicit impls ++ spc() ++
       str (conjugate_to_be impls) ++ str" implicit" ++
       (if max then strbrk " and maximally inserted" else mt())) ++ fnl()
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 61f7e377a2..a9dd471d65 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -306,7 +306,7 @@ let pr_evgl_sign gl =
   let ids = List.rev (List.map pi1 l) in
   let warn =
     if ids = [] then mt () else
-      (str "(" ++ prlist_with_sep pr_coma pr_id ids ++ str " cannot be used)")
+      (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
   in
   let pc = pr_lconstr gl.evar_concl in
   hov 0 (str"[" ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]" ++ spc () ++ warn)