[doc] terminology loader/importer

doc/userman/user-acsl.tex

@@ -106,7 +106,7 @@ used, it is possible to have logic identifiers with an extended lexical format:
   For instance, \verb+Foo::bar'jazz+ is a syntactically valid identifier.
 \end{itemize}
 
-External module loaders are defined by plug-ins \textit{via} the extension API,
+External module importers are defined by plug-ins \textit{via} the extension API,
 consult the plug-in manuals and the plug-in developer manual for more details.
 
 %%% Local Variables:

src/plugins/wp/Why3Import.ml

@@ -345,7 +345,7 @@ module Env = WpContext.StaticGenerator
         add_builtins env ; env
     end)
 
-let loader (ctxt: LT.module_builder) (_: C.location) (m: string list) =
+let importer (ctxt: LT.module_builder) (_: C.location) (m: string list) =
   begin
     L.debug ~dkey "Importing Why3 theory %s.@." (String.concat "::" m) ;
     let thname = String.concat "." m in
@@ -360,7 +360,7 @@ let register () =
   if not !registered then
     begin
       registered := true ;
-      Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader ;
+      Acsl_extension.register_module_importer ~plugin:"wp" "why3" importer ;
     end
 
 let () = Cmdline.run_after_extended_stage register

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -1788,13 +1788,13 @@ by a link (`\user{link};'). The available tags are depicted on figure~\ref{wp-dr
 \subsection{Importing Why3 Modules}
 \label{importer}
 
-The \textsf{WP} plug-in provides an \textsf{ACSL} module loader that
+The \textsf{WP} plug-in provides an \textsf{ACSL} module importer that
 can import \textsf{Why3} theories and modules into \textsf{ACSL}.
 See \textsf{Frama-C} user manual, Section § 6.3 for details.
 Here is an example of use:
 
 \begin{lstlisting}
-//@ import why3: number::Gcd;
+//@ import \wp::why3: number::Gcd;
 
 /*@
   assigns \nothing;