Fix some issues with the comments

8 files changed, 19 insertions, 22 deletions

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index 7fba3c5c..e751d0ba 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -8,7 +8,7 @@
     
     TODO: implementing the concrete evaluation functions for the
     assumed functions is really annoying (see
-    {!InterpreterStatements.eval_non_local_function_call_concrete}),
+    [InterpreterStatements.eval_non_local_function_call_concrete]),
     I think it should be possible, in most situations, to write bodies which
     model the behaviour of those unsafe functions. For instance, [Box::deref_mut]
     should simply be:
diff --git a/compiler/Config.ml b/compiler/Config.ml
index f446872c..1f91645b 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -1,6 +1,6 @@
 (** Define the global configuration options *)
 
-(** {0 Interpreter} *)
+(** {1 Interpreter} *)
 
 (** Check that invariants are maintained whenever we execute a statement *)
 let check_invariants = ref true
@@ -44,7 +44,7 @@ let allow_bottom_below_borrow = true
  *)
 let return_unit_end_abs_with_no_loans = true
 
-(** {0 Translation} *)
+(** {1 Translation} *)
 
 (** Controls whether we need to use a state to model the external world
     (I/O, for instance).
@@ -59,7 +59,7 @@ let use_state = ref true (* TODO *)
        (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
        ...
        (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
-    }]
+    ]}
 
     Otherwise, we generate code of the following shape:
     {[
@@ -110,7 +110,7 @@ let extract_decreases_clauses = ref true
  *)
 let extract_template_decreases_clauses = ref false
 
-(** {0 Micro passes} *)
+(** {1 Micro passes} *)
 
 (** Some provers like F* don't support the decomposition of return values
     in monadic let-bindings:
@@ -141,8 +141,8 @@ let decompose_monadic_let_bindings = ref false
 
     This is useful when extracting to F*: the support for monadic
     definitions is not super powerful.
-    Note that when {!field:unfold_monadic_let_bindings} is true, setting
-    {!field:decompose_monadic_let_bindings} to true and only makes the code
+    Note that when {!unfold_monadic_let_bindings} is true, setting
+    {!decompose_monadic_let_bindings} to true and only makes the code
     more verbose.
  *)
 let unfold_monadic_let_bindings = ref false
@@ -173,7 +173,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 {!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/Cps.ml b/compiler/Cps.ml
index c2c0363b..de35198f 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -67,7 +67,7 @@ let comp_update (f : cm_fun) (g : C.eval_ctx -> C.eval_ctx) : cm_fun =
 
 (** This is just a test, to check that {!comp} is general enough to handle a case
     where a function must compute a value and give it to the continuation.
-    It happens for functions like {!InterpreterExpressions.eval_operand}.
+    It happens for functions like {!val:InterpreterExpressions.eval_operand}.
 
     Keeping this here also makes it a good reference, when one wants to figure
     out the signatures he should use for such a composition.
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index a268ed1f..fa717041 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -17,7 +17,7 @@ open InterpreterPaths
     borrows*.
 
     This function doesn't reorganize the context to make sure we can read
-    the place. If needs be, you should call {!update_ctx_along_read_place} first.
+    the place. If needs be, you should call {!InterpreterPaths.update_ctx_along_read_place} first.
  *)
 val read_place : access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun
 
@@ -64,8 +64,8 @@ val eval_operands :
 
     Transmits the computed rvalue to the received continuation.
 
-    Note that this function fails on {!E.Discriminant}: discriminant reads should
-    have been eliminated from the AST.
+    Note that this function fails on {!constructor:E.Discriminant}: discriminant
+    reads should have been eliminated from the AST.
  *)
 val eval_rvalue_not_global :
   C.config -> E.rvalue -> ((V.typed_value, eval_error) result -> m_fun) -> m_fun
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fc18dbd3..fda2b3a6 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -48,7 +48,7 @@ let option_none_id = T.option_none_id
 type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
 [@@deriving show, ord]
 
-(** Ancestor for iter visitor for {!Pure.ty} *)
+(** Ancestor for iter visitor for [ty] *)
 class ['self] iter_ty_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
@@ -57,7 +57,7 @@ class ['self] iter_ty_base =
     method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for map visitor for {!Pure.ty} *)
+(** Ancestor for map visitor for [ty] *)
 class ['self] map_ty_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
@@ -498,9 +498,9 @@ and meta =
 type fun_effect_info = {
   stateful_group : bool;
       (** [true] if the function group is stateful. By *function group*, we mean
-          the set { forward function } U { backward functions }.
+          the set [{ forward function } U { backward functions }].
 
-          We need this because the option {!Translate.eval_config.backward_no_state_update}:
+          We need this because of the option {!Config.backward_no_state_update}:
           if it is [true], then in case of a backward function {!stateful} is [false],
           but we might need to know whether the corresponding forward function
           is stateful or not.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1bf3b903..132dc02e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1083,7 +1083,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
 (** Decompose the monadic let-bindings.
 
-    See the explanations in {!config.decompose_monadic_let_bindings}
+    See the explanations in {!Config.decompose_monadic_let_bindings}
  *)
 let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
     fun_decl =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 1ab3439c..0f16b5b4 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -73,7 +73,7 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
   in
   fun id -> TypeVarId.Map.find id mp
 
-(** Retrieve the list of fields for the given variant of a {!type_decl}.
+(** Retrieve the list of fields for the given variant of a {!type:Pure.type_decl}.
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index fafcb348..a327c785 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -485,10 +485,7 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
   let abs_ids = list_ancestor_abstractions_ids ctx abs in
   List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids
 
-(** Small utility.
-
-    [backward_no_state_update]: see {!config}
- *)
+(** Small utility. *)
 let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info =
   match fun_id with