diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/coqlib.ml | 4 | ||||
| -rw-r--r-- | interp/genarg.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1528589841..9ca0a41bd0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -257,7 +257,7 @@ let set_var_scope loc id (_,_,scopt,scopes) varscopes = | [] -> str "the empty scope stack" | [a] -> str "scope " ++ str a | l -> str "scope stack " ++ - str "[" ++ prlist_with_sep pr_coma str l ++ str "]" in + str "[" ++ prlist_with_sep pr_comma str l ++ str "]" in user_err_loc (loc,"set_var_scope", pr_id id ++ str " is used both in " ++ pr_scope_stack (make_current_scope (Option.get !idscopes)) ++ diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 8a4bc63650..54a1d61491 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -51,12 +51,12 @@ let gen_constant_in_modules locstr dirs s = | [] -> anomalylabstrm "" (str (locstr^": cannot find "^s^ " in module"^(if List.length dirs > 1 then "s " else " ")) ++ - prlist_with_sep pr_coma pr_dirpath dirs) + prlist_with_sep pr_comma pr_dirpath dirs) | l -> anomalylabstrm "" (str (locstr^": found more than once object of name "^s^ " in module"^(if List.length dirs > 1 then "s " else " ")) ++ - prlist_with_sep pr_coma pr_dirpath dirs) + prlist_with_sep pr_comma pr_dirpath dirs) (* For tactics/commands requiring vernacular libraries *) diff --git a/interp/genarg.ml b/interp/genarg.ml index e5950cd8d6..707769a55c 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -103,7 +103,7 @@ let rec pr_intro_pattern (_,pat) = match pat with and pr_or_and_intro_pattern = function | [pl] -> - str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" + str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")" | pll -> str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) |