Commit 60b16cd3 authored by MARCHE Claude's avatar MARCHE Claude

Documentation of Call_provers module

parent 1fa84dd8
......@@ -1601,7 +1601,7 @@ MODULESTODOC = \
util/weakhtbl util/stdlib util/rc util/debug \
core/ident core/ty core/term core/decl core/theory \
core/env core/task \
driver/whyconf driver/driver \
driver/whyconf driver/call_provers driver/driver \
session/session session/session_tools session/session_scheduler \
whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \
whyml/mlw_main
......
......@@ -11,7 +11,9 @@
open Model_parser
(** Call provers and parse their outputs *)
(** {1 Call provers and parse their outputs} *)
(** {2 data types for prover answers} *)
type prover_answer =
| Valid
......@@ -83,6 +85,7 @@ type prover_result_parser = {
prp_model_parser : Model_parser.model_parser;
}
(** {2 Functions for calling external provers} *)
type prover_call
(** Type that represents a single prover run *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment