diff options
| author | ppedrot | 2012-06-04 17:18:31 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-04 17:18:31 +0000 |
| commit | 0f500f2e7a3164df44a2b20e67550cb0072d8948 (patch) | |
| tree | 9847b7c9d731864df0ad8a9d732fd7780a448a60 /interp | |
| parent | 12f77536d29e6b6eeb2f1d065a805d353d197de9 (diff) | |
Replacing some str with strbrk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 6 | ||||
| -rw-r--r-- | interp/topconstr.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 90b495982e..9389a1690b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -315,8 +315,8 @@ let implicits_of_glob_constr ?(with_products=true) l = if with_products then abs na bk b else (if bk = Implicit then - msg_warning (str "Ignoring implicit status of product binder " ++ - pr_name na ++ str " and following binders"); + msg_warning (strbrk "Ignoring implicit status of product binder " ++ + pr_name na ++ strbrk " and following binders"); []) | GLambda (loc, na, bk, t, b) -> abs na bk b | GLetIn (loc, na, t, b) -> aux i b diff --git a/interp/notation.ml b/interp/notation.ml index 64911675b8..2430b980ca 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -156,14 +156,14 @@ let declare_delimiters scope key = | Some oldkey when oldkey = key -> () | Some oldkey -> Flags.if_warn msg_warning - (str ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); + (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); scope_map := Gmap.add scope newsc !scope_map end; try let oldscope = Gmap.find key !delimiters_map in if oldscope = scope then () else begin - Flags.if_warn msg_warning (str ("Hiding binding of key "^key^" to "^oldscope)); + Flags.if_warn msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); delimiters_map := Gmap.add key scope !delimiters_map end with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map @@ -317,7 +317,7 @@ let declare_notation_interpretation ntn scopt pat df = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if Gmap.mem ntn sc.notations then - Flags.if_warn msg_warning (str ("Notation "^ntn^" was already used"^ + Flags.if_warn msg_warning (strbrk ("Notation "^ntn^" was already used"^ (if scopt = None then "" else " in scope "^scope))); let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in scope_map := Gmap.add scope sc !scope_map; diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1036baf7c1..9b3c00bf22 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -138,7 +138,7 @@ let fold_constr_expr_with_binders g f n acc = function fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (loc,_,_) -> - msg_warning (str "Capture check in multiple binders not done"); acc + msg_warning (strbrk "Capture check in multiple binders not done"); acc let free_vars_of_constr_expr c = let rec aux bdvars l = function |