diff options
| author | ppedrot | 2012-05-30 16:05:13 +0000 |
|---|---|---|
| committer | ppedrot | 2012-05-30 16:05:13 +0000 |
| commit | 24879dc0e59856e297b0172d00d67df67fbb0184 (patch) | |
| tree | d57ffef43297aa7f8b29830f3bde7f3bd334babb /pretyping | |
| parent | f9d97c62b2e46829a6ece74d07f5fab2cea1d769 (diff) | |
More uniformisation in Pp.warn functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index fd20f199c8..a3fe0d059c 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 warning "Detyping.detype: cannot factorize fix enough"; + if n>0 then msg_warning (str "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) |