diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4a907b2795..91cd5b251c 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -309,9 +309,15 @@ END ~category:"deprecated" ~default:CWarnings.Enabled (fun () -> (Pp.strbrk - "SSReflect's Search command has been moved to the \ - ssrsearch module; please Require that module if you \ - still want to use SSReflect's Search command")) + "In previous versions of Coq, loading SSReflect had the effect of \ + replacing the built-in 'Search' command with an SSReflect version \ + of that command. \ + Coq's own search feature was still available via 'SearchAbout' \ + (but that alias is deprecated). \ + This replacement no longer happens; now 'Search' calls Coq's own search \ + feature even when SSReflect is loaded. \ + If you want to use SSReflect's deprecated Search command \ + instead of the built-in one, please Require the ssrsearch module.")) open G_vernac } |