Fix the issues with the cross-references for OCaml doc

16 files changed, 35 insertions, 35 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1a00656d..364ef748 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -289,7 +289,7 @@ let unfold_monadic_let_bindings = ref false
     we later filter the useless *forward* calls in the micro-passes, where it is
     more natural to do.
 
-    See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths}
+    See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths}
     for additional explanations.
  *)
 let filter_useless_monadic_calls = ref true
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a2ae4f16..c93bb213 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -112,7 +112,7 @@ let reset_global_counters () =
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
-(** Ancestor for {!env} iter visitor *)
+(** Ancestor for {!type:env} iter visitor *)
 class ['self] iter_env_base =
   object (_self : 'self)
     inherit [_] iter_abs
@@ -120,7 +120,7 @@ class ['self] iter_env_base =
     method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for {!env} map visitor *)
+(** Ancestor for {!type:env} map visitor *)
 class ['self] map_env_base =
   object (_self : 'self)
     inherit [_] map_abs
@@ -423,11 +423,11 @@ let erase_regions (ty : ty) : ty =
   in
   v#visit_ty () ty
 
-(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *)
+(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
   ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
 
-(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *)
+(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 1ca68120..85ab1112 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -311,7 +311,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
     the same name because Lean uses the typing information to resolve the
     ambiguities.
 
-    This map complements the {!names_map}, which checks for collisions.
+    This map complements the {!type:names_map}, which checks for collisions.
   *)
 type unsafe_names_map = { id_to_name : string IdMap.t }
 
@@ -1639,7 +1639,7 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
       function is an assumed function or a local function
     - function basename
     - the number of loops in the parent function. This is used for
-      the same purpose as in {!field:llbc_name}.
+      the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
 let ctx_compute_termination_measure_name (ctx : extraction_ctx)
@@ -1668,7 +1668,7 @@ let ctx_compute_termination_measure_name (ctx : extraction_ctx)
       function is an assumed function or a local function
     - function basename
     - the number of loops in the parent function. This is used for
-      the same purpose as in {!field:llbc_name}.
+      the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
 let ctx_compute_decreases_proof_name (ctx : extraction_ctx)
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index c6212d31..ca9984be 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -213,7 +213,7 @@ let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
     - in Lean, groups of mutually recursive definitions must end with "end"
     - in HOL4 (in most situations) the whole group must be within a `Define` command
 
-    Calls to {!extract_fun_decl} should be inserted between calls to
+    Calls to {!Extract.extract_fun_decl} should be inserted between calls to
     {!start_fun_decl_group} and {!end_fun_decl_group}.
 
     TODO: maybe those [{start/end}_decl_group] functions are not that much a good
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index b13d545c..44f85d0a 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -924,7 +924,7 @@ let remove_intersecting_aproj_borrows_shared (regions : RegionId.Set.t)
         
     [subst]: takes as parameters the abstraction in which we perform the
     substitution and the list of given back values at the projector of
-    loans where we perform the substitution (see the fields in {!AProjLoans}).
+    loans where we perform the substitution (see the fields in {!Values.AProjLoans}).
     Note that the symbolic value at this place is necessarily equal to [sv],
     which is why we don't give it as parameters.
  *)
@@ -970,13 +970,13 @@ let update_intersecting_aproj_loans (proj_regions : RegionId.Set.t)
   (* Return *)
   ctx
 
-(** Helper function: lookup an {!AProjLoans} by using an abstraction id and a
+(** Helper function: lookup an {!constructor:Values.aproj.AProjLoans} by using an abstraction id and a
     symbolic value.
-    
+
     We return the information from the looked up projector of loans. See the
-    fields in {!AProjLoans} (we don't return the symbolic value, because it
+    fields in {!constructor:Values.aproj.AProjLoans} (we don't return the symbolic value, because it
     is equal to [sv]).
-    
+
     Sanity check: we check that there is exactly one projector which corresponds
     to the couple (abstraction id, symbolic value).
  *)
@@ -1115,7 +1115,7 @@ let update_aproj_borrows (abs_id : AbstractionId.id) (sv : symbolic_value)
 
 (** Helper function: might break invariants.
 
-    Converts an {!AProjLoans} to an {!AEndedProjLoans}. The projector is identified
+    Converts an {!Values.aproj.AProjLoans} to an {!Values.aproj.AEndedProjLoans}. The projector is identified
     by a symbolic value and an abstraction id.
  *)
 let update_aproj_loans_to_ended (abs_id : AbstractionId.id)
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index 4be1fd24..b545f979 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -79,6 +79,6 @@ val expand_symbolic_int :
   m_fun
 
 (** If this mode is activated through the [config], greedily expand the symbolic
-    values which need to be expanded. See {!type:config} for more information.
+    values which need to be expanded. See {!type:Contexts.config} for more information.
  *)
 val greedy_expand_symbolic_values : config -> cm_fun
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index d14230c6..ca1f8f31 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -41,10 +41,10 @@ type abs_borrows_loans_maps = {
   borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t;
 }
 
-(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}.
+(** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher].
 
     This module contains primitive match functions to instantiate the generic
-    {!InterpreterLoopsMatchCtxs.MakeMatcher} functor.
+    {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor.
   *)
 module type PrimMatcher = sig
   val match_etys : ety -> ety -> ety
@@ -231,8 +231,8 @@ module type Matcher = sig
     eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
 end
 
-(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
-    {!InterpreterLoopsCore.CheckEquivMatcher}.
+(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
+    {!module-type:InterpreterLoopsCore.CheckEquivMatcher}.
 
     Very annoying: functors only take modules as inputs...
  *)
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index bf29af79..5f69b8d3 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -27,13 +27,13 @@ val compute_abs_borrows_loans_maps :
     We use it for joins, to check if two environments are convertible, etc.
     See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}.
 
-    The functor is parameterized by a {!PrimMatcher}, which implements the
-    non-generic part of the match. More precisely, the role of {!PrimMatcher} is two
+    The functor is parameterized by a {!module-type:InterpreterLoopsCore.PrimMatcher}, which implements the
+    non-generic part of the match. More precisely, the role of {!module-type:InterpreterLoopsCore.PrimMatcher} is two
     provide generic functions which recursively match two values (by recursively
     matching the fields of ADT values for instance). When it does need to match
     values in a non-trivial manner (if two ADT values don't have the same
     variant for instance) it calls the corresponding specialized function from
-    {!PrimMatcher}.
+    {!module-type:InterpreterLoopsCore.PrimMatcher}.
  *)
 module MakeMatcher : functor (_ : PrimMatcher) -> Matcher
 
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 583c6907..9e4ebc20 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -6,7 +6,7 @@ open Contexts
 
     Apply a proj_borrows on a shared borrow.
     Note that when projecting over shared values, we generate
-    {!type:abstract_shared_borrows}, not {!type:avalue}s.
+    {!type:Aeneas.Values.abstract_shared_borrows}, not {!type:Aeneas.Values.avalue}s.
 
     Parameters:
     [regions]
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index d84e8be6..3832d02f 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -10,7 +10,7 @@ open Cps
     dummy variables, after ending the proper borrows of course) but the return
     variable, move the return value out of the return variable, remove all the
     local variables (but preserve the abstractions!), remove the
-    {!constructor:env_elem.Frame} indicator delimiting the current frame and
+    {!constructor:Contexts.env_elem.EFrame} indicator delimiting the current frame and
     handle the return value to the continuation.
 
     If the boolean is false, we don't move the return value, and call the
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index ecd8f53f..bba88e9f 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -111,7 +111,7 @@ let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
 (** Create a loans projector value from a symbolic value.
     
     Checks if the projector will actually project some regions. If not,
-    returns {!AIgnored} ([_]).
+    returns {!Values.AIgnored} ([_]).
     
     TODO: update to handle 'static
  *)
@@ -238,7 +238,7 @@ let symbolic_value_has_ended_regions (ended_regions : RegionId.Set.t)
   let regions = ty_regions s.sv_ty in
   not (RegionId.Set.disjoint regions ended_regions)
 
-(** Check if a {!type:value} contains [⊥].
+(** Check if a {!type:Values.value} contains [⊥].
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 50849df9..0ae83007 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -273,7 +273,7 @@ class virtual ['self] mapreduce_ty_base =
 
 type ty =
   | TAdt of type_id * generic_args
-      (** {!Adt} encodes ADTs and tuples and assumed types.
+      (** {!TAdt} encodes ADTs and tuples and assumed types.
 
           TODO: what about the ended regions? (ADTs may be parameterized
           with several region variables. When giving back an ADT value, we may
@@ -1064,7 +1064,7 @@ type trait_impl = {
   meta : meta;
   impl_trait : trait_decl_ref;
   llbc_impl_trait : Types.trait_decl_ref;
-      (** Same remark as for {llbc_generics}. *)
+      (** Same remark as for {!field:llbc_generics}. *)
   generics : generic_params;
   llbc_generics : Types.generic_params;
       (** We use the LLBC generics to generate "pretty" names, for instance
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6b0deb73..a5143f3c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -195,7 +195,7 @@ let fun_sig_substitute (subst : subst) (sg : fun_sig) : inst_fun_sig =
     We only look for outer monadic let-bindings.
     This is used when printing the branches of [if ... then ... else ...].
 
-    Rem.: this function will *fail* if there are {!constructor:Aeneas.Pure.expression.Loop}
+    Rem.: this function will *fail* if there are {!Pure.Loop}
     nodes (you should call it on an expression where those nodes have been eliminated).
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 73e7f71d..a05b2c5a 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -76,7 +76,7 @@ let erase_regions_subst : subst =
     tr_self = Self;
   }
 
-(** Convert an {!rty} to an {!ety} by erasing the region variables *)
+(** Erase the region variables in a type *)
 let erase_regions (ty : ty) : ty = ty_substitute erase_regions_subst ty
 
 let trait_ref_erase_regions (tr : trait_ref) : trait_ref =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index a9f45926..53f99b7f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -66,8 +66,8 @@ type 'a region_group_id_map = 'a RegionGroupId.Map.t [@@deriving show]
 
 (** Ancestor for {!expression} iter visitor.
 
-    We could make it inherit the visitor for {!eval_ctx}, but in all the uses
-    of this visitor we don't need to explore {!eval_ctx}, so we make it inherit
+    We could make it inherit the visitor for {!Contexts.eval_ctx}, but in all the uses
+    of this visitor we don't need to explore {!Contexts.eval_ctx}, so we make it inherit
     the abstraction visitors instead.
  *)
 class ['self] iter_expression_base =
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index 52e12b9a..76cc710a 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -5,7 +5,7 @@ include Charon.TypesUtils
 (** Retuns true if the type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
+    we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
@@ -15,7 +15,7 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
 (** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
+    we erase the lists of regions (by replacing them with [[]] when using {!type:Types.ty},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_nested_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =