aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml2
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/coqlib.ml4
-rw-r--r--interp/genarg.ml2
-rw-r--r--kernel/mod_subst.ml2
-rw-r--r--kernel/univ.ml6
-rw-r--r--lib/rtree.ml4
-rw-r--r--lib/util.ml4
-rw-r--r--lib/util.mli2
-rw-r--r--library/declare.ml6
-rw-r--r--parsing/ppconstr.ml6
-rw-r--r--parsing/pptactic.ml14
-rw-r--r--parsing/prettyp.ml2
-rw-r--r--parsing/printer.ml2
-rw-r--r--plugins/decl_mode/ppdecl_proof.ml4
-rw-r--r--plugins/firstorder/g_ground.ml46
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/subtac/subtac_utils.ml2
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/inv.ml2
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/himsg.ml6
-rw-r--r--toplevel/metasyntax.ml2
-rw-r--r--toplevel/record.ml2
24 files changed, 44 insertions, 44 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d1893005d..286f596e4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -68,7 +68,7 @@ let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Intset.elements l))
let ppidset l = pp (prset pr_id (Idset.elements l))
-let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_coma pr l) ++ str "]"
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
let ppidmap pr l =
let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in
pp (prset' pr (Idmap.fold (fun a b l -> (a,b)::l) l []))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 152858984..9ca0a41bd 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 8a4bc6365..54a1d6149 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 e5950cd8d..707769a55 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)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index c967bf1ba..d0f855a32 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -274,7 +274,7 @@ let debug_pr_subst sub =
let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++
spc () ++ str "[" ++ str s3 ++ str "]")
in
- str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}"
+ str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}"
let subst_mp0 sub mp = (* 's like subst *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ca0d8fbd0..50de9a054 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -78,9 +78,9 @@ let pr_uni = function
str "(" ++ pr_uni_level u ++ str ")+1"
| Max (gel,gtl) ->
str "max(" ++ hov 0
- (prlist_with_sep pr_coma pr_uni_level gel ++
- (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
- prlist_with_sep pr_coma
+ (prlist_with_sep pr_comma pr_uni_level gel ++
+ (if gel <> [] & gtl <> [] then pr_comma () else mt ()) ++
+ prlist_with_sep pr_comma
(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
str ")"
diff --git a/lib/rtree.ml b/lib/rtree.ml
index b1c934506..e7934c45e 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -173,11 +173,11 @@ let rec pp_tree prl t =
| Node(lab,[||]) -> hov 2 (str"("++prl lab++str")")
| Node(lab,v) ->
hov 2 (str"("++prl lab++str","++brk(1,0)++
- Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str")")
+ Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str")")
| Rec(i,v) ->
if Array.length v = 0 then str"Rec{}"
else if Array.length v = 1 then
hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}")
else
hov 2 (str"Rec{"++int i++str","++brk(1,0)++
- Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str"}")
+ Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str"}")
diff --git a/lib/util.ml b/lib/util.ml
index 42cdc2bf2..ea5da9e3c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1194,7 +1194,7 @@ let pr_spc = spc
let pr_fnl = fnl
let pr_int = int
let pr_str = str
-let pr_coma () = str "," ++ spc ()
+let pr_comma () = str "," ++ spc ()
let pr_semicolon () = str ";" ++ spc ()
let pr_bar () = str "|" ++ spc ()
let pr_arg pr x = spc () ++ pr x
@@ -1242,7 +1242,7 @@ let rec pr_sequence elem = function
let pr_enum pr l =
let c,l' = list_sep_last l in
- prlist_with_sep pr_coma pr l' ++
+ prlist_with_sep pr_comma pr l' ++
(if l'<>[] then str " and" ++ spc () else mt()) ++ pr c
let pr_vertical_list pr = function
diff --git a/lib/util.mli b/lib/util.mli
index 43dd43913..8c811d439 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -316,7 +316,7 @@ val pr_spc : unit -> std_ppcmds
val pr_fnl : unit -> std_ppcmds
val pr_int : int -> std_ppcmds
val pr_str : string -> std_ppcmds
-val pr_coma : unit -> std_ppcmds
+val pr_comma : unit -> std_ppcmds
val pr_semicolon : unit -> std_ppcmds
val pr_bar : unit -> std_ppcmds
val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
diff --git a/library/declare.ml b/library/declare.ml
index 68b9ca9fb..b571ecf3a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -288,11 +288,11 @@ let fixpoint_message indexes l =
(match indexes with
| Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
| _ -> mt ())
- | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+ | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
spc () ++ str "are recursively defined" ++
match indexes with
| Some a -> spc () ++ str "(decreasing respectively on " ++
- prlist_with_sep pr_coma pr_rank (Array.to_list a) ++
+ prlist_with_sep pr_comma pr_rank (Array.to_list a) ++
str " arguments)"
| None -> mt ()))
@@ -300,7 +300,7 @@ let cofixpoint_message l =
Flags.if_verbose msgnl (match l with
| [] -> anomaly "No corecursive definition."
| [id] -> pr_id id ++ str " is corecursively defined"
- | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+ | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
spc () ++ str "are corecursively defined"))
let recursive_message isfix i l =
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index cf5a58eea..2d63b20bb 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 9714b7fa9..f410e38f3 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 882a94ffb..cc04f8f34 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 61f7e377a..a9dd471d6 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)
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 5bd15b93f..e8a8ac226 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 77f15aa07..26929bbd2 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 81c7c29d2..fc8f7ac96 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 32a1755ca..06a80f68a 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 =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2d18c36fe..3efa9b218 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -345,7 +345,7 @@ ARGUMENT EXTEND hintbases
| [ ] -> [ Some [] ]
END
-let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_coma prc
+let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc
ARGUMENT EXTEND constr_coma_sequence
TYPED AS constr_list
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 3130c1ca9..e732a31c4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -50,7 +50,7 @@ let check_no_metas clenv ccl =
errorlabstrm "inversion"
(str ("Cannot find an instantiation for variable"^
(if List.length metas = 1 then " " else "s ")) ++
- prlist_with_sep pr_coma pr_name metas
+ prlist_with_sep pr_comma pr_name metas
(* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *))
let var_occurs_in_pf gl id =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 005052df2..d20c213c4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -188,7 +188,7 @@ type structured_inductive_expr =
let minductive_message = function
| [] -> error "No inductive definition."
| [x] -> (pr_id x ++ str " is defined")
- | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+ | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
spc () ++ str "are defined")
let check_all_names_different indl =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 39c545589..bccde6cbd 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -569,7 +569,7 @@ let explain_refiner_bad_type arg ty conclty =
let explain_refiner_unresolved_bindings l =
str "Unable to find an instance for the " ++
str (plural (List.length l) "variable") ++ spc () ++
- prlist_with_sep pr_coma pr_name l ++ str"."
+ prlist_with_sep pr_comma pr_name l ++ str"."
let explain_refiner_cannot_apply t harg =
str "In refiner, a term of type" ++ brk(1,1) ++
@@ -655,7 +655,7 @@ let error_same_names_constructors id =
let error_same_names_overlap idl =
strbrk "The following names are used both as type names and constructor " ++
str "names:" ++ spc () ++
- prlist_with_sep pr_coma pr_id idl ++ str "."
+ prlist_with_sep pr_comma pr_id idl ++ str "."
let error_not_an_arity id =
str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity."
@@ -827,7 +827,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
quote (pr_rawconstr_env (Global.env()) c) ++
(if unboundvars <> [] or vars <> [] then
strbrk " (with " ++
- prlist_with_sep pr_coma
+ prlist_with_sep pr_comma
(fun (id,c) ->
pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
(List.rev vars @ unboundvars) ++ str ")"
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 443ed4853..6dda11405 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -673,7 +673,7 @@ let pr_arg_level from = function
let pr_level ntn (from,args) =
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
- prlist_with_sep pr_coma (pr_arg_level from) args
+ prlist_with_sep pr_comma (pr_arg_level from) args
let error_incompatible_level ntn oldprec prec =
errorlabstrm ""
diff --git a/toplevel/record.ml b/toplevel/record.ml
index d95c3657e..e4177b0fc 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -94,7 +94,7 @@ let warning_or_error coe indsp err =
let s,have = if List.length projs > 1 then "s","were" else "","was" in
(str(string_of_id fi) ++
strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
- prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++
+ prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++
strbrk " not defined.")
| BadTypedProj (fi,ctx,te) ->
match te with
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 20:12:18 +0000