diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -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 86921c49b..cc178eb97 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t = share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough"); + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); let c = detype flags avoid env sigma c in let t = detype flags avoid env sigma t in (List.rev l,c,t) |