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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 12 |
4 files changed, 9 insertions, 9 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a3fe0d059c..b6d460a85d 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -490,7 +490,7 @@ and share_names isgoal n l avoid env c t = share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then msg_warning (str "Detyping.detype: cannot factorize fix enough"); + if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); let c = detype isgoal avoid env c in let t = detype isgoal avoid env t in (List.rev l,c,t) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e9d6a3c29a..0bd9e95ac4 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -160,7 +160,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match dest_recarg ra with | Mrec (_,j) when is_rec -> (depPvect.(j),rest) | Imbr _ -> - Flags.if_warn msg_warning (str "Ignoring recursive call"); + Flags.if_warn msg_warning (strbrk "Ignoring recursive call"); (None,rest) | _ -> (None, rest)) in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1e73e26342..77d9cd963a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -273,7 +273,7 @@ let rec pat_of_raw metas vars = function PMeta None | GCast (_,c,_) -> Flags.if_warn - Pp.msg_warning (str "Cast not taken into account in constr pattern"); + Pp.msg_warning (strbrk "Cast not taken into account in constr pattern"); pat_of_raw metas vars c | GIf (_,c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e2b03d0f22..7cecec1578 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -245,9 +245,9 @@ let compute_canonical_projections (con,ind) = if Flags.is_verbose () then (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in - msg_warning (str "No global reference exists for projection value" - ++ Termops.print_constr t ++ str " in instance " - ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it.")); + msg_warning (strbrk "No global reference exists for projection value" + ++ Termops.print_constr t ++ strbrk " in instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")); l end | _ -> l) @@ -279,9 +279,9 @@ let open_canonical_structure i (_,o) = and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Idset.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - msg_warning (str "Ignoring canonical projection to " ++ hd_val - ++ str " by " ++ prj ++ str " in " - ++ new_can_s ++ str ": redundant with " ++ old_can_s)) lo + msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val + ++ strbrk " by " ++ prj ++ strbrk " in " + ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo let cache_canonical_structure o = open_canonical_structure 1 o |