diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.ml | 11 | ||||
| -rw-r--r-- | interp/notation.ml | 26 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 |
3 files changed, 20 insertions, 19 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 02504c920..5ac718e3b 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s = match these with | [x] -> x | [] -> - anomaly ~label:locstr (str ("cannot find "^s^ - " in module"^(if List.length dirs > 1 then "s " else " ")) ++ + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) | l -> anomaly ~label:locstr - (str ("ambiguous name "^s^" can represent ") ++ + (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) let gen_constant_in_modules locstr dirs s = @@ -86,7 +86,8 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(DirPath.to_string dir)^" has to be required first.") + errorlabstrm "Coqlib.check_required_library" + (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/interp/notation.ml b/interp/notation.ml index 80db2cb39..555dfa804 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -91,7 +91,9 @@ let declare_scope scope = (* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map -let error_unknown_scope sc = error ("Scope "^sc^" is not declared.") +let error_unknown_scope sc = + errorlabstrm "Notation" + (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = try String.Map.find scope !scope_map @@ -186,14 +188,14 @@ let declare_delimiters scope key = | Some oldkey when String.equal oldkey key -> () | Some oldkey -> msg_warning - (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); + (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map end; try let oldscope = String.Map.find key !delimiters_map in if String.equal oldscope scope then () else begin - msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); + msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); delimiters_map := String.Map.add key scope !delimiters_map end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map @@ -202,7 +204,7 @@ let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> user_err_loc - (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^".")) + (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".") (* Uninterpretation tables *) @@ -317,8 +319,7 @@ let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> user_err_loc (loc,"prim_token_interpreter", - str ("Cannot interpret in "^sc^" without requiring first module " - ^(List.last d)^".")) + str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -373,10 +374,9 @@ let declare_notation_interpretation ntn scopt pat df = let () = if String.Map.mem ntn sc.notations then let which_scope = match scopt with - | None -> "" - | Some _ -> " in scope " ^ scope in - let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in - msg_warning (strbrk message) + | None -> mt () + | Some _ -> str " in scope " ++ str scope in + msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) in let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in let () = scope_map := String.Map.add scope sc !scope_map in @@ -452,7 +452,7 @@ let interp_notation loc ntn local_scopes = try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err_loc - (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) + (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -784,8 +784,8 @@ let pr_scope_classes sc = match l with | [] -> mt () | _ :: l -> - let opt_s = match l with [] -> "" | _ -> "es" in - hov 0 (str ("Bound to class" ^ opt_s) ++ + let opt_s = match l with [] -> mt () | _ -> str "es" in + hov 0 (str "Bound to class" ++ opt_s ++ spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl() let pr_notation_info prglob ntn c = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 9be7abcfe..d2709d5e3 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -99,7 +99,7 @@ let verbose_compat kn def = function | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r | _ -> str " is a compatibility notation" in - let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in + let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in act (pr_syndef kn ++ pp_def ++ since) | _ -> () |