diff --git a/Makefile.in b/Makefile.in
index fe7224543d314467c628d87b049ff7942d104e56..12c80ec14800f1b0b601184160af9fff09440a25 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1822,16 +1822,28 @@ doc/bnf$(EXE): doc/bnf.mll
 	$(OCAMLLEX) $<
 	$(OCAMLC) -o $@ doc/bnf.ml
 
+doc/extract_ocaml_code: doc/extract_ocaml_code.ml
+	$(OCAMLC) str.cma -o $@ $<
+
 doc/logic_%.ml: examples/use_api/logic.ml doc/extract_ocaml_code
 	doc/extract_ocaml_code examples/use_api/logic.ml $* doc
 
+doc/whyconf_%.ml: src/driver/whyconf.ml doc/extract_ocaml_code
+	doc/extract_ocaml_code src/driver/whyconf.ml $* doc
+
+doc/call_provers_%.ml: src/driver/call_provers.ml doc/extract_ocaml_code
+	doc/extract_ocaml_code src/driver/call_provers.ml $* doc
+
 OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \
-	buildtask printtask buildtask2
+	buildtask printtask buildtask2 \
+	getconf getanyaltergo getaltergo200 \
+	getdriver callprover calltimelimit
 
-OCAMLCODE = $(addprefix doc/logic_, $(addsuffix .ml, $(OCAMLCODE_LOGIC)))
+OCAMLCODE_CALLPROVERS = proveranswer proverresult resourcelimit
 
-doc/extract_ocaml_code: doc/extract_ocaml_code.ml
-	$(OCAMLC) str.cma -o $@ $<
+OCAMLCODE = $(addprefix doc/logic_, $(addsuffix .ml, $(OCAMLCODE_LOGIC))) \
+	$(addprefix doc/call_provers_, $(addsuffix .ml, $(OCAMLCODE_CALLPROVERS))) \
+	doc/whyconf_provertype.ml
 
 DOC = api glossary ide intro exec macros manpages install \
       manual starting syntax syntaxref technical version whyml \
diff --git a/doc/api.tex b/doc/api.tex
index 640df9a1ce7740124416215ea17c9693a4b052cc..8d4de0e2d8a4c56420f40a9abc49b2ef226c64fc 100644
--- a/doc/api.tex
+++ b/doc/api.tex
@@ -117,125 +117,135 @@ file \texttt{why3.conf}, as it was built using the \texttt{why3config}
 command line tool or the \textsf{Detect Provers} menu of the graphical
 IDE. The following API calls allow to access the content of this
 configuration file.
-\begin{ocamlcode}
-(* reads the config file *)
-let config : Whyconf.config = Whyconf.read_config None
-(* the [main] section of the config file *)
-let main : Whyconf.main = Whyconf.get_main config
-(* all the provers detected, from the config file *)
-let provers : Whyconf.config_prover Whyconf.Mprover.t =
-  Whyconf.get_provers config
-\end{ocamlcode}
+% \begin{ocamlcode}
+% (* reads the config file *)
+% let config : Whyconf.config = Whyconf.read_config None
+% (* the [main] section of the config file *)
+% let main : Whyconf.main = Whyconf.get_main config
+% (* all the provers detected, from the config file *)
+% let provers : Whyconf.config_prover Whyconf.Mprover.t =
+%   Whyconf.get_provers config
+% \end{ocamlcode}
+\lstinputlisting{logic_getconf.ml}
 The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
 prover is a record with a name, a version, and an alternative description
 (to differentiate between various configurations of a given prover). Its
 definition is in the module \texttt{Whyconf}:
-\begin{ocamlcode}
-type prover =
-    { prover_name : string; (* "Alt-Ergo" *)
-      prover_version : string; (* "2.95" *)
-      prover_altern : string; (* "special" *)
-    }
-\end{ocamlcode}
+% \begin{ocamlcode}
+% type prover =
+%     { prover_name : string; (* "Alt-Ergo" *)
+%       prover_version : string; (* "2.95" *)
+%       prover_altern : string; (* "special" *)
+%     }
+% \end{ocamlcode}
+\lstinputlisting{whyconf_provertype.ml}
 The map \texttt{provers} provides the set of existing provers.
 In the following, we directly
-attempt to access the prover Alt-Ergo, which is known to be identified
-with id \texttt{"alt-ergo"}.
-\begin{ocamlcode}
-(* the [prover alt-ergo] section of the config file *)
-let alt_ergo : Whyconf.config_prover =
-  try
-    Whyconf.prover_by_id config "alt-ergo"
-  with Whyconf.ProverNotFound _ ->
-    eprintf "Prover alt-ergo not installed or not configured@.";
-    exit 0
-\end{ocamlcode}
+attempt to access a prover named ``Alt-Ergo'', any version.
+% \begin{ocamlcode}
+% (* the [prover alt-ergo] section of the config file *)
+% let alt_ergo : Whyconf.config_prover =
+%   try
+%     Whyconf.prover_by_id config "alt-ergo"
+%   with Whyconf.ProverNotFound _ ->
+%     eprintf "Prover alt-ergo not installed or not configured@.";
+%     exit 0
+% \end{ocamlcode}
+\lstinputlisting{logic_getanyaltergo.ml}
 We could also get a specific version with :
-\begin{ocamlcode}
-let alt_ergo : Whyconf.config_prover =
-  try
-    let prover = {Whyconf.prover_name = "Alt-Ergo";
-                  prover_version = "0.92.3";
-                  prover_altern = ""} in
-    Whyconf.Mprover.find prover provers
-  with Not_found ->
-    eprintf "Prover alt-ergo not installed or not configured@.";
-    exit 0
-\end{ocamlcode}
+% \begin{ocamlcode}
+% let alt_ergo : Whyconf.config_prover =
+%   try
+%     let prover = {Whyconf.prover_name = "Alt-Ergo";
+%                   prover_version = "2.0.0";
+%                   prover_altern = ""} in
+%     Whyconf.Mprover.find prover provers
+%   with Not_found ->
+%     eprintf "Prover Alt-Ergo 2.0.0 not installed or not configured@.";
+%     exit 0
+% \end{ocamlcode}
+\lstinputlisting{logic_getaltergo200.ml}
 
 The next step is to obtain the driver associated to this prover. A
 driver typically depends on the standard theories so these should be
 loaded first.
-\begin{ocamlcode}
-(* builds the environment from the [loadpath] *)
-let env : Env.env =
-  Env.create_env (Whyconf.loadpath main)
-(* loading the Alt-Ergo driver *)
-let alt_ergo_driver : Driver.driver =
-  try
-    Driver.load_driver env alt_ergo.Whyconf.driver
-  with e ->
-    eprintf "Failed to load driver for alt-ergo: %a@."
-      Exn_printer.exn_printer e;
-    exit 1
-\end{ocamlcode}
+% \begin{ocamlcode}
+% (* builds the environment from the [loadpath] *)
+% let env : Env.env =
+%   Env.create_env (Whyconf.loadpath main)
+% (* loading the Alt-Ergo driver *)
+% let alt_ergo_driver : Driver.driver =
+%   try
+%     Driver.load_driver env alt_ergo.Whyconf.driver
+%   with e ->
+%     eprintf "Failed to load driver for alt-ergo: %a@."
+%       Exn_printer.exn_printer e;
+%     exit 1
+% \end{ocamlcode}
+\lstinputlisting{logic_getdriver.ml}
 
 We are now ready to call the prover on the tasks. This is done by a
 function call that launches the external executable and waits for its
 termination. Here is a simple way to proceed:
-\begin{ocamlcode}
-(* calls Alt-Ergo *)
-let result1 : Call_provers.prover_result =
-  Call_provers.wait_on_call
-    (Driver.prove_task ~command:alt_ergo.Whyconf.command
-    alt_ergo_driver task1 ()) ()
-(* prints Alt-Ergo answer *)
-let () = printf "@[On task 1, alt-ergo answers %a@]@."
-  Call_provers.print_prover_result result1
-\end{ocamlcode}
+% \begin{ocamlcode}
+% (* calls Alt-Ergo *)
+% let result1 : Call_provers.prover_result =
+%   Call_provers.wait_on_call
+%     (Driver.prove_task ~command:alt_ergo.Whyconf.command
+%     alt_ergo_driver task1 ()) ()
+% (* prints Alt-Ergo answer *)
+% let () = printf "@[On task 1, alt-ergo answers %a@]@."
+%   Call_provers.print_prover_result result1
+% \end{ocamlcode}
+\lstinputlisting{logic_callprover.ml}
 This way to call a prover is in general too naive, since it may never
 return if the prover runs without time limit. The function
-\texttt{prove\_task} has two optional parameters: \texttt{timelimit}
-is the maximum allowed running time in seconds, and \texttt{memlimit}
-is the maximum allowed memory in megabytes.  The type
-\texttt{prover\_result} is a record with three fields:
+\texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined
+in module \texttt{Call\_provers}:
+\lstinputlisting{call_provers_resourcelimit.ml}
+where the field \texttt{limit\_time} is the maximum allowed running time in seconds,
+and \texttt{limit\_mem} is the maximum allowed memory in megabytes.  The type
+\texttt{prover\_result} is a record defined in module \texttt{Call\_provers}:
+\lstinputlisting{call_provers_proverresult.ml}
+with in particular the fields:
 \begin{itemize}
 \item \texttt{pr\_answer}: the prover answer, explained below;
-\item \texttt{pr\_output}: the output of the prover, \ie both
-  standard output and the standard error of the process
-  (a redirection in \texttt{why3.conf} is required);
 \item \texttt{pr\_time} : the time taken by the prover, in seconds.
 \end{itemize}
-A \texttt{pr\_answer} is a sum of several kind of answers:
+A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}:
+\lstinputlisting{call_provers_proveranswer.ml}
+corresponding to these kinds of answers:
 \begin{itemize}
 \item \texttt{Valid}: the task is valid according to the prover.
 \item \texttt{Invalid}: the task is invalid.
-\item \texttt{Timeout}: the prover exceeds the time or memory limit.
+\item \texttt{Timeout}: the prover exceeds the time limit.
+\item \texttt{OutOfMemory}: the prover exceeds the memory limit.
 \item \texttt{Unknown} $msg$: the prover can't determine if the task
   is valid; the string parameter $msg$ indicates some extra
   information.
-\item \texttt{Failure} $msg$: the prover reports a failure, \ie it
+\item \texttt{Failure} $msg$: the prover reports a failure, \eg it
   was unable to read correctly its input task.
 \item \texttt{HighFailure}: an error occurred while trying to call the
-  prover, or the prover answer was not understood (\ie none of the
+  prover, or the prover answer was not understood (\eg none of the
   given regular expressions in the driver file matches the output
   of the prover).
 \end{itemize}
 Here is thus another way of calling the Alt-Ergo prover, on our second
 task.
-\begin{ocamlcode}
-let result2 : Call_provers.prover_result =
-   Call_provers.wait_on_call
-    (Driver.prove_task ~command:alt_ergo.Whyconf.command
-    ~timelimit:10
-    alt_ergo_driver task2 ()) ()
-
-let () =
-  printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
-    Call_provers.print_prover_answer
-    result1.Call_provers.pr_answer
-    result1.Call_provers.pr_time
-\end{ocamlcode}
+% \begin{ocamlcode}
+% let result2 : Call_provers.prover_result =
+%    Call_provers.wait_on_call
+%     (Driver.prove_task ~command:alt_ergo.Whyconf.command
+%     ~timelimit:10
+%     alt_ergo_driver task2 ()) ()
+
+% let () =
+%   printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
+%     Call_provers.print_prover_answer
+%     result1.Call_provers.pr_answer
+%     result1.Call_provers.pr_time
+% \end{ocamlcode}
+\lstinputlisting{logic_calltimelimit.ml}
 The output of our program is now as follows.
 \begin{verbatim}
 On task 1, alt-ergo answers Valid (0.01s)
diff --git a/examples/use_api/logic.ml b/examples/use_api/logic.ml
index d2eb7f841c031fcd69e81baa815c4bbc21a99a6a..abd3ef62453615d78b20d7db7c14535f9e982619 100644
--- a/examples/use_api/logic.ml
+++ b/examples/use_api/logic.ml
@@ -77,6 +77,7 @@ let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2
 
 (* To call a prover, we need to access the Why configuration *)
 
+(* BEGIN{getconf} *)
 (* reads the config file *)
 let config : Whyconf.config = Whyconf.read_config None
 (* the [main] section of the config file *)
@@ -84,7 +85,9 @@ let main : Whyconf.main = Whyconf.get_main config
 (* all the provers detected, from the config file *)
 let provers : Whyconf.config_prover Whyconf.Mprover.t =
   Whyconf.get_provers config
+(* END{getconf} *)
 
+(* BEGIN{getanyaltergo} *)
 (* One prover named Alt-Ergo in the config file *)
 let alt_ergo : Whyconf.config_prover =
   let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
@@ -95,7 +98,21 @@ let alt_ergo : Whyconf.config_prover =
     exit 0
   end else
     snd (Whyconf.Mprover.max_binding provers)
+(* END{getanyaltergo} *)
 
+(* BEGIN{getaltergo200} *)
+(* Specific version 2.0.0 of Alt-Ergo in the config file *)
+let alt_ergo_2_0_0 : Whyconf.config_prover =
+  let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.0.0" in
+  let provers = Whyconf.filter_provers config fp in
+  if Whyconf.Mprover.is_empty provers then begin
+    eprintf "Prover Alt-Ergo 2.0.0 not installed or not configured@.";
+    exit 0
+  end else
+    snd (Whyconf.Mprover.max_binding provers)
+(* END{getaltergo200} *)
+
+(* BEGIN{getdriver} *)
 (* builds the environment from the [loadpath] *)
 let env : Env.env = Env.create_env (Whyconf.loadpath main)
 
@@ -107,7 +124,9 @@ let alt_ergo_driver : Driver.driver =
     eprintf "Failed to load driver for alt-ergo: %a@."
       Exn_printer.exn_printer e;
     exit 1
+(* END{getdriver} *)
 
+(* BEGIN{callprover} *)
 (* calls Alt-Ergo *)
 let result1 : Call_provers.prover_result =
   Call_provers.wait_on_call
@@ -116,9 +135,11 @@ let result1 : Call_provers.prover_result =
     alt_ergo_driver task1)
 
 (* prints Alt-Ergo answer *)
-let () = printf "@[On task 1, alt-ergo answers %a@."
+let () = printf "@[On task 1, Alt-Ergo answers %a@."
   Call_provers.print_prover_result result1
+(* END{callprover} *)
 
+(* BEGIN{calltimelimit} *)
 let result2 : Call_provers.prover_result =
   Call_provers.wait_on_call
     (Driver.prove_task ~command:alt_ergo.Whyconf.command
@@ -128,6 +149,7 @@ let result2 : Call_provers.prover_result =
 let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
   Call_provers.print_prover_answer result1.Call_provers.pr_answer
   result1.Call_provers.pr_time
+(* END{calltimelimit} *)
 
 
 
diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml
index 303e5f885603b8f5a8abf29a62961ec69c7179a6..72fb16fa29e12fbb420a7a994ba031ddf6d44a58 100644
--- a/src/driver/call_provers.ml
+++ b/src/driver/call_provers.ml
@@ -22,6 +22,7 @@ type reason_unknown =
   | Resourceout
   | Other
 
+(* BEGIN{proveranswer} anchor for automatic documentation, do not remove *)
 type prover_answer =
   | Valid
   | Invalid
@@ -31,7 +32,9 @@ type prover_answer =
   | Unknown of (string * reason_unknown option)
   | Failure of string
   | HighFailure
+(* END{proveranswer} anchor for automatic documentation, do not remove *)
 
+(* BEGIN{proverresult} anchor for automatic documentation, do not remove *)
 type prover_result = {
   pr_answer : prover_answer;
   pr_status : Unix.process_status;
@@ -40,12 +43,15 @@ type prover_result = {
   pr_steps  : int;		(* -1 if unknown *)
   pr_model  : model;
 }
+(* END{proverresult} anchor for automatic documentation, do not remove *)
 
+(* BEGIN{resourcelimit} anchor for automatic documentation, do not remove *)
 type resource_limit = {
   limit_time  : int;
   limit_mem   : int;
   limit_steps : int;
 }
+(* END{resourcelimit} anchor for automatic documentation, do not remove *)
 
 let empty_limit = { limit_time = 0 ; limit_mem = 0; limit_steps = 0 }
 
diff --git a/src/driver/whyconf.ml b/src/driver/whyconf.ml
index 3772ba04e0f38e65aa58e7a556c9f5dc0d3d1e00..c5b0d3ebd47854c273aa7f7d9b426d1a7e323264 100644
--- a/src/driver/whyconf.ml
+++ b/src/driver/whyconf.ml
@@ -52,11 +52,13 @@ let default_conf_file =
 
 (* Prover *)
 
+(* BEGIN{provertype} anchor for automatic documentation, do not remove *)
 type prover =
     { prover_name : string;
       prover_version : string;
       prover_altern : string;
     }
+(* END{provertype} anchor for automatic documentation, do not remove *)
 
 let print_altern fmt s =
   if s <> "" then Format.fprintf fmt " (%s)" s