diff options
| author | herbelin | 2010-06-12 15:30:28 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-12 15:30:28 +0000 |
| commit | a885a2148e4d45606c654145db5d859c4d6a223b (patch) | |
| tree | 5feb549d45868e5eab7762891d0e7dc46f4e7760 /plugins | |
| parent | d30267620672a939f56fb9d6e161070bbb1112a6 (diff) | |
Fixing spelling: pr_coma -> pr_comma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 4 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 6 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 5bd15b93fa..e8a8ac2267 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -77,7 +77,7 @@ and print_vars pconstr gtyp env sep _be _have vars = match st.st_label with Anonymous -> anomaly "anonymous variable" | Name id -> Environ.push_named (id,None,st.st_it) env in - let pr_sep = if sep then pr_coma () else mt () in + let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ pr_statement pr_constr env st ++ print_vars pconstr gtyp nenv true _be _have rest @@ -143,7 +143,7 @@ let rec pr_bare_proof_instr _then _thus env = function str "given" ++ print_vars pr_constr _I env false false "given" hyps | Ptake witl -> str "take" ++ spc () ++ - prlist_with_sep pr_coma (pr_constr env) witl + prlist_with_sep pr_comma (pr_constr env) witl | Pdefine (id,args,body) -> str "define" ++ spc () ++ pr_id id ++ spc () ++ prlist_with_sep spc diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 77f15aa07a..26929bbd25 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -106,9 +106,9 @@ let normalize_evaluables= open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_coma pr_reference -let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_coma (pr_or_var (pr_located pr_global)) -let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_coma pr_global +let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference +let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global)) +let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global ARGUMENT EXTEND firstorder_using TYPED AS reference_list diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 81c7c29d22..fc8f7ac966 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -112,7 +112,7 @@ TACTIC EXTEND snewfunind END -let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc +let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_comma prc ARGUMENT EXTEND constr_coma_sequence' TYPED AS constr_list diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 32a1755ca0..06a80f68a8 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -365,7 +365,7 @@ let recursive_message v = match Array.length v with | 0 -> error "no recursive definition" | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined") - | _ -> hov 0 (prvect_with_sep pr_coma (Printer.pr_constant (Global.env ())) v ++ + | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++ spc () ++ str "are recursively defined") let print_message m = |