Skip to content

Commit

Permalink
Fix links in odoc mld files (#756)
Browse files Browse the repository at this point in the history
  • Loading branch information
bclement-ocp authored Jul 26, 2023
1 parent 6504947 commit 4d11f96
Show file tree
Hide file tree
Showing 5 changed files with 15 additions and 15 deletions.
1 change: 1 addition & 0 deletions src/bin/common/dune
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
)

(library
(package alt-ergo)
(name alt_ergo_common)
(libraries
alt-ergo-lib
Expand Down
10 changes: 6 additions & 4 deletions src/bin/common/index_common.mld
Original file line number Diff line number Diff line change
@@ -1,23 +1,25 @@
{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}

The command line parsing is done with {{:https://erratique.ch/software/cmdliner}[cmdliner]} in the module {!module:Alt_ergo_common.Parse_command}. This module initialises options of the Alt-Ergo-Lib library.

{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}
12 changes: 7 additions & 5 deletions src/bin/text/index.mld
Original file line number Diff line number Diff line change
Expand Up @@ -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]}.
7 changes: 1 addition & 6 deletions src/parsers/index.mld
Original file line number Diff line number Diff line change
Expand Up @@ -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]}.
File renamed without changes.

0 comments on commit 4d11f96

Please sign in to comment.