From 07ec165220792ad133637cec250bf64d8520111f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 26 Jul 2023 15:36:39 +0200 Subject: [PATCH] Fix links in odoc mld files --- src/bin/common/dune | 1 + src/bin/common/index_common.mld | 10 ++++++---- src/bin/text/index.mld | 12 +++++++----- src/parsers/index.mld | 7 +------ src/plugins/AB-Why3/{index_abwhy3.mld => index.mld} | 0 5 files changed, 15 insertions(+), 15 deletions(-) rename src/plugins/AB-Why3/{index_abwhy3.mld => index.mld} (100%) diff --git a/src/bin/common/dune b/src/bin/common/dune index 795a9a45c..9c56361e4 100644 --- a/src/bin/common/dune +++ b/src/bin/common/dune @@ -4,6 +4,7 @@ ) (library + (package alt-ergo) (name alt_ergo_common) (libraries alt-ergo-lib diff --git a/src/bin/common/index_common.mld b/src/bin/common/index_common.mld index 9663dbc72..69b725175 100644 --- a/src/bin/common/index_common.mld +++ b/src/bin/common/index_common.mld @@ -1,8 +1,10 @@ {1 Alt_ergo_common} +See also the {{:Alt_ergo_common/index.html}list of modules}. + {2 Main Solving } -The solving loop is done in the {!module:Alt_ergo_common.solving_loop} module. This module uses the registered input method (parser and typechecker) to compute the input file (see {!section:input}). It relies on initialised options (see {!section:cmdline}). +The solving loop is done in the {!Alt_ergo_common.Solving_loop} module. This module uses the registered input method (parser and typechecker) to compute the input file (see {!section:input}). It relies on initialised options (see {!section:cmdline}). {2:cmdline Command line parsing} @@ -10,14 +12,14 @@ The command line parsing is done with {{:https://erratique.ch/software/cmdliner} {2:input Input Frontend } -The {!module:Alt_ergo_common.input_frontend} module register an input method capable of parsing and typechecking the input files +The {!module:Alt_ergo_common.Input_frontend} module register an input method capable of parsing and typechecking the input files The legacy frontend is used to parse and typecheck file with the native Alt-Ergo syntaxe and also the smtlib2 and psmt2 syntaxe. {2:signals Signals and profiling } -The {!module:Alt_ergo_common.signals_profiling} module initialise handlers for system signals and profiling informations and timers. +The {!module:Alt_ergo_common.Signals_profiling} module initialise handlers for system signals and profiling informations and timers. {2:dynlink Stdlib wrapper} -{!modules:Alt_ergo_common.MyDynlink} +See {!Alt_ergo_common.MyDynlink} diff --git a/src/bin/text/index.mld b/src/bin/text/index.mld index bd452abf3..390dff19c 100644 --- a/src/bin/text/index.mld +++ b/src/bin/text/index.mld @@ -9,14 +9,16 @@ is available through the {e --help} option. This package uses the Alt-Ergo_common internal lib (see {{:index_common.html}[Alt_ergo_common]}) for parsing command line, input file, and main solving loop. +See also the {{:Alt_ergo_common/index.html}list of modules}. + {3 Plugins} {4 Why3 parser} -for the Why3 parser plugin documentation see -{{:index_abwhy3.html} - [ABWhy3]} +For the Why3 parser plugin documentation see +{{:../alt-ergo-plugin-ab-why3/index.html} + [ABWhy3]}. {4 Fourier Motzkin simplex} -for the Fourier Motzkin simplex plugin documentation see +For the Fourier Motzkin simplex plugin documentation see {{:index_fmsimplex.html} - [FMsimplex]} + [FMsimplex]}. diff --git a/src/parsers/index.mld b/src/parsers/index.mld index b96e518a6..ae57fc2e1 100644 --- a/src/parsers/index.mld +++ b/src/parsers/index.mld @@ -25,10 +25,5 @@ Users can add new parsers to Alt-Ergo with the option [--add-parser]. This parser should have the same interface as {!module-type:AltErgoParsers.Parsers.PARSER_INTERFACE} and should be registered using {!val:AltErgoParsers.Parsers.register_parser} {4 Why3 parser plugin} -see {{:../alt-ergo/index_abwhy3.html}[ABWhy3]} - -{2 Utilities} -{!modules: -AltErgoParsers.MyZip -} +See {{:../alt-ergo-plugin-ab-why3/index.html}[the ABWhy3 plugin]}. diff --git a/src/plugins/AB-Why3/index_abwhy3.mld b/src/plugins/AB-Why3/index.mld similarity index 100% rename from src/plugins/AB-Why3/index_abwhy3.mld rename to src/plugins/AB-Why3/index.mld