Fix dead links and compilation warnings in sphinx doc

docs/sphinx_docs/Input_file_formats/Native/00_summary.md

@@ -23,13 +23,13 @@
 Reserved keywords are the following.
 * To add new uninterpreted symbols (variables or functions) to the signature: [`logic`](01_declaration_of_symbols.md#logic-uninterpreted-symbols) and the [`ac` modifier](01_declaration_of_symbols.md#ac-modifier-associative-and-commutative-symbols) for associative and commutative symbols.
 * Interpreted functions: [`function`](01_declaration_of_symbols.md#function-user-defined-functions) and [`predicate`](01_declaration_of_symbols.md#predicate-propositional-valued-functions).
-* Built-in types: [`int`](02_types/02_01_builtin.md#numbers-int-real-and-floats), [`real`](02_types/02_01_builtin.md#numbers-int-real-and-floats), [`bool`](02_types/02_01_builtin.md#bool-and-prop), [`prop`](02_types/02_01_builtin.md#bool-and-prop), [`unit`](02_types/02_01_builtin.md#unit), [`bitv`](02_types/02_01_builtin.md#bitvectors-bitv), [`farray`](02_types/02_01_builtin.md#functional-polymorphic-arrays-farray).
+* Built-in types: [`int`](02_types/02_01_builtin.md#numeric-types), [`real`](02_types/02_01_builtin.md#numeric-types), [`bool`](02_types/02_01_builtin.md#boolean-types), [`prop`](02_types/02_01_builtin.md#boolean-types), [`unit`](02_types/02_01_builtin.md#unit-type), [`bitv`](02_types/02_01_builtin.md#bitvectors), [`farray`](02_types/02_01_builtin.md#polymorphic-functional-arrays).
 * Constant and operators for propositions are available: `and`, `or`, `xor`, `not`, `true`, `false`. The construct `distinct` is available for all types. Quantifiers `forall` and `exists` can be used.
 * To create new types: [`type`](02_types/index). They keyword `of` is useful when dealing with structured datatypes, which include [records](02_types/02_02_user_defined.md#records), [enums](02_types/02_02_user_defined.md#enums-and-algebraic-datatypes) and [algebraic datatypes](02_types/02_02_user_defined.md#enums-and-algebraic-datatypes).
 * To declare new axioms: [`axiom`](03_declaration_of_axioms.md#axiom), and the special case [`rewriting`](03_declaration_of_axioms.md#rewriting).
 * To define goals that must be proven valid: [`goal`](04_setting_goals.md#goal). [`cut`](04_setting_goals.md#intermediate-goals-cut-and-check) and [`check`](04_setting_goals.md#intermediate-goals-cut-and-check) can create intermediate goals that won't interact with other goals through [triggers](03_declaration_of_axioms.md#triggers).
-* New theories may be defined using [theory](05_theories.md#theory-extends-end) (and the keywords `extends` and `end`). Inside theories, [`axiom`](05_theories.md#axiom) can be used with [additional triggers](05_theories.md#semantic-triggers). The construct [`case_split`](05_theories.md#case-split) is also available.
-* Other useful constructs are [`let` [...] `in`](06_control_flow.md#let-in), [`match` [...] `with` [...] `end`](06_control_flow.md#match-with) and [`if` [...] `then` [...] `else` [...]](06_control_flow.md#if-then-else).
+* New theories may be defined using [theory](05_theories.md#user-defined-extensions-of-theories) (and the keywords `extends` and `end`). Inside theories, [`axiom`](03_declaration_of_axioms.md#axiom) can be used with [additional triggers](05_theories.md#semantic-triggers). The construct [`case_split`](05_theories.md#case_split) is also available.
+* Other useful constructs are [`let` [...] `in`](06_control_flow.md#let--in), [`match` [...] `with` [...] `end`](06_control_flow.md#match--with) and [`if` [...] `then` [...] `else` [...]](06_control_flow.md#if--then--else).
 
 The list of all reserved keywords, in alphabetical order, is:
 ```

docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

@@ -53,6 +53,7 @@ Creation and manipulation of values having those types are covered in [built-in
 
 For all those operators, `bool` and `prop` are fully interchangeable.
 
+(the-bool-prop-conflict)=
 #### The `bool`/`prop` conflict
 
 Prior to Alt-Ergo 2.3.0, Alt-Ergo's native language handled differently boolean variables `bool` and propositional variables `prop`.

docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md

@@ -11,13 +11,13 @@ The heuristic for choosing new instances is based on *triggers*. By default, tri
 In order to declare an axiom, the user can use the following construct.
 Note that axioms must always be named.
 
-#### Syntax
+### Syntax
 ```
 <axiom_declaration> ::= 'axiom' <id> ':' <axiom_body>
 ```
 Here, `<axiom_body>` is an expression which may contain quantifiers, and where user-specified triggers may be added to universal quantifiers.
 
-#### Example
+### Example
 
 ```
 (* Axioms can be used without quantifiers *)
@@ -56,7 +56,7 @@ Interval triggers further restrict instantiation of axioms, and check that varia
 
 Multiple patterns can be used in syntactic triggers. They are separated by `|` which means 'or' and by `,` which means 'and'. `|` has an higher precedence than `,`.
 
-#### Syntax
+### Syntax
 ```
 <quantified_formula>    ::= <quantifier> <var_id_list_sep_comma> ':' <var_type> <syntactic_triggers>? <interval_triggers>? '.' <expr>
 <quantifier>            ::= 'exists' | 'forall'
@@ -75,9 +75,9 @@ Interval triggers also exists. [TODO: add more explanations]
 <rel>                   ::= '<' | '<='
 ```
 
-[Semantic triggers](05_theories.html#semantic-triggers) are only available in theories
+[Semantic triggers](05_theories.md#semantic-triggers) are only available in theories
 
-#### Examples
+### Examples
 ```
 (* P(x) used as the only trigger *)
 logic P,Q,R: int -> prop
@@ -110,13 +110,13 @@ To add a new axiom directly in the form of a rewriting technique, the keyword `r
 
 [TODO: complete]
 
-#### Syntax
+### Syntax
 ```
 <rewriting_declaraction> ::= 'rewriting' <id> ':' <predicate_list_sep_pv>
 <predicate_list_sep_pv>  ::= <predicate> (';' <predicate_list_sep_pv>? )? 
 (* pre-written objects of type predicate can be used, as well as expressions that can be interpreted as predicates *) 
 <predicate>              ::= <predicate_expr> | <predicate_id>
 ```
 
-#### Example
+### Example
 [TODO: find relevant examples]

docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md

@@ -9,13 +9,13 @@ Alt-Ergo will answer `Valid` if it can prove that the formula of the goal is tru
 To declare goals, the user can use the following construct.
 Note that goals must always be named.
 
-#### Syntax
+### Syntax
 ```
 <goal_declaration> ::= 'goal' <id> ':' <goal_body>
 ```
 Here, `<goal_body>` is an expression which may contain quantifiers.
 
-#### Examples
+### Examples
 ```
 logic h, g, f: int, int -> int
 logic a, b:int
@@ -44,7 +44,7 @@ In other word, `cut` and `check` allow to test if intermediate goals can be prov
 
 [WIP: complete]
 
-#### Syntax
+### Syntax
 ```
 <check_declaration> ::= 'check' <expr>
 <cut_declaration>   ::= 'cut' <expr>

docs/sphinx_docs/Input_file_formats/Native/05_theories.md

@@ -54,7 +54,7 @@ More information on this strategy and the language extension can be found in [th
 
 ### Semantic triggers
 
-In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in [section Axioms](03_declaration_of_axioms.md), additional triggers are available inside theories.
+In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in [axioms](03_declaration_of_axioms.md), additional triggers are available inside theories.
 Those additional triggers are called semantic triggers.
 
 They correspond to the following constructs.

docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md

@@ -7,13 +7,13 @@
 Like in OCaml, let expressions are available. They allow for named local expressions, which are written `let name = expression in [...]`.
 Name defined like this only have local scope.
 
-#### Syntax
+### Syntax
 ```
 <let_expression>       ::= 'let' <let_binders> 'in' <expr>
 <let_binders>          ::= <id> '=' <expr> ( ',' <id> '=' <expr> )*
 ```
 
-#### Example
+### Example
 ```
 function average(a:real, b:real):real =
     let sum = a+b in
@@ -27,15 +27,15 @@ Pattern matching, a [Really Cool Feature](https://ocaml.org/learn/tutorials/data
 Warning: the only patterns that can be matched are constructors of algebraic datatypes.
 Moreover, constructors can't be nested in a pattern.
 
-#### Syntax
+### Syntax
 ```
 <match_expr>     ::= 'match' <expr> 'with' <match_cases> 'end'
 <match_cases>    ::= '|'? <simple_pattern> '->' <expr> ( '|' <simple_pattern> '->' <expr> )*
 <simple_pattern> ::= <id> | <id_application> '(' <args> ')'
 <args>           ::= <id> ( "," <id> )*
 ```
 
-#### Example
+### Example
 ```
 type 'a tree = NIL | Node of { left:'a tree; val:'a; right:'a tree }
 
@@ -53,7 +53,7 @@ function height(t: 'a tree):int =
 
 The simple construct `if then else` for conditional expressions is available in Alt-Ergo's native language.
 
-#### Syntax
+### Syntax
 ```
 <ite_expr>     ::= 'if' <cond_expr> 'then' <branch1_expr> 'else' <branch2_expr>
 (* Note that <cond_expr> must have type bool - or prop *)
@@ -63,7 +63,7 @@ The simple construct `if then else` for conditional expressions is available in
 <branch2_expr> ::= <expr>
 ```
 
-#### Example
+### Example
 ```
 function max(a:int, b:int):int =
     if a>b then a else b