diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml
index 602defe1f..dadb906db 100644
--- a/infer/src/IR/Exp.ml
+++ b/infer/src/IR/Exp.ml
@@ -110,7 +110,7 @@ let rec root_of_lexp lexp =
 
 
 (** Checks whether an expression denotes a location by pointer arithmetic.
-    Currently, catches array - indexing expressions such as a[i] only. *)
+    Currently, catches array-indexing expressions such as a[i] only. *)
 let rec pointer_arith = function
   | Lfield (e, _, _) ->
       pointer_arith e
diff --git a/infer/src/biabduction/Match.ml b/infer/src/biabduction/Match.ml
index 8c4ee026c..07602e490 100644
--- a/infer/src/biabduction/Match.ml
+++ b/infer/src/biabduction/Match.ml
@@ -19,8 +19,8 @@ let mem_idlist i l = List.exists ~f:(Ident.equal i) l
     considered during pattern matching *)
 type hpred_pat = {hpred: Sil.hpred; flag: bool}
 
-(** Checks e1 = e2[sub ++ sub'] for some sub' with dom(sub') subseteq vars.
-    Returns (sub ++ sub', vars - dom(sub')). *)
+(** Checks [e1 = e2[sub ++ sub']] for some [sub'] with [dom(sub') subseteq vars].
+    Returns [(sub ++ sub', vars - dom(sub'))]. *)
 let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
   let check_equal sub vars e1 e2 =
     let e2_inst = Sil.exp_sub sub e2 in
@@ -93,8 +93,8 @@ let exp_list_match es1 sub vars es2 =
     (List.zip es1 es2)
 
 
-(** Checks sexp1 = sexp2[sub ++ sub'] for some sub' with
-    dom(sub') subseteq vars. Returns (sub ++ sub', vars - dom(sub')).
+(** Checks [sexp1 = sexp2[sub ++ sub']] for some [sub'] with
+    [dom(sub') subseteq vars]. Returns [(sub ++ sub', vars - dom(sub'))].
     WARNING: This function does not consider the fact that the analyzer
     sometimes forgets fields of hpred. It can possibly cause a problem. *)
 let rec strexp_match sexp1 sub vars sexp2 : (Sil.subst * Ident.t list) option =
@@ -115,8 +115,8 @@ let rec strexp_match sexp1 sub vars sexp2 : (Sil.subst * Ident.t list) option =
         None )
 
 
-(** Checks fsel1 = fsel2[sub ++ sub'] for some sub' with
-    dom(sub') subseteq vars. Returns (sub ++ sub', vars - dom(sub')). *)
+(** Checks [fsel1 = fsel2[sub ++ sub']] for some [sub'] with
+    [dom(sub') subseteq vars]. Returns [(sub ++ sub', vars - dom(sub'))]. *)
 and fsel_match fsel1 sub vars fsel2 =
   match (fsel1, fsel2) with
   | [], [] ->
@@ -139,8 +139,8 @@ and fsel_match fsel1 sub vars fsel2 =
       else None
 
 
-(** Checks isel1 = isel2[sub ++ sub'] for some sub' with
-    dom(sub') subseteq vars. Returns (sub ++ sub', vars - dom(sub')). *)
+(** Checks [isel1 = isel2[sub ++ sub']] for some [sub'] with
+    [dom(sub') subseteq vars]. Returns [(sub ++ sub', vars - dom(sub'))]. *)
 and isel_match isel1 sub vars isel2 =
   match (isel1, isel2) with
   | [], [] ->
@@ -543,8 +543,8 @@ and hpara_dll_match_with_impl tenv impl_ok para1 para2 : bool =
 
 (** [prop_match_with_impl p condition vars hpat hpats]
     returns [(subst, p_leftover)] such that
-    1) [dom(subst) = vars]
-    2) [p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover].
+    + [dom(subst) = vars]
+    + [p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover].
     Using the flag [field], we can control the strength of |-. *)
 let prop_match_with_impl tenv p condition vars hpat hpats =
   prop_match_with_impl_sub tenv p condition Sil.sub_empty vars hpat hpats
diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index e2ab4053d..6506d3717 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -531,7 +531,7 @@ let sigma_get_unsigned_exps sigma =
 
 
 (** Collapse consecutive indices that should be added. For instance,
-    this function reduces x[1][1] to x[2]. The [typ] argument is used
+    this function reduces [x[1][1]] to [x[2]]. The [typ] argument is used
     to ensure the soundness of this collapsing. *)
 let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp =
   let typ_is_base (typ1 : Typ.t) =
diff --git a/infer/src/biabduction/Prop.mli b/infer/src/biabduction/Prop.mli
index 05dba8270..7b57ba61b 100644
--- a/infer/src/biabduction/Prop.mli
+++ b/infer/src/biabduction/Prop.mli
@@ -141,7 +141,7 @@ val exp_normalize_noabs : Tenv.t -> Sil.subst -> Exp.t -> Exp.t
 
 val exp_collapse_consecutive_indices_prop : Typ.t -> Exp.t -> Exp.t
 (** Collapse consecutive indices that should be added. For instance,
-    this function reduces x[1][1] to x[2]. The [typ] argument is used
+    this function reduces [x[1][1]] to [x[2]]. The [typ] argument is used
     to ensure the soundness of this collapsing. *)
 
 val lexp_normalize_prop : Tenv.t -> 'a t -> Exp.t -> Exp.t
diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml
index 79423e967..ce89a25f3 100644
--- a/infer/src/biabduction/Tabulation.ml
+++ b/infer/src/biabduction/Tabulation.ml
@@ -474,7 +474,7 @@ let check_path_errors_in_post tenv caller_pname post post_path =
 
 
 (** Post process the instantiated post after the function call so that
-    x.f |-> se becomes x |-> \{ f: se \}.
+    x.f |-> se becomes x |-> { f: se }.
     Also, update any Aresource attributes to refer to the caller *)
 let post_process_post tenv caller_pname callee_pname loc actual_pre
     ((post : Prop.exposed Prop.t), post_path) =
diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli
index ccc605670..2a03145b2 100644
--- a/infer/src/checkers/accessPathDomains.mli
+++ b/infer/src/checkers/accessPathDomains.mli
@@ -20,11 +20,11 @@ module Set : sig
   val of_list : AccessPath.Abs.t list -> astate
 
   val mem : AccessPath.Abs.t -> astate -> bool
-  (** return true if \gamma(\{ap\}) \subseteq \gamma(aps).
+  (** return true if {% \gamma(\{ap\}) \subseteq \gamma(aps) %}.
       note: this is worst-case linear in the size of the set *)
 
   val mem_fuzzy : AccessPath.Abs.t -> astate -> bool
-  (** more permissive version of [mem]; return true if \gamma(\{a\}) \cap \gamma(aps) != \{\}.
+  (** more permissive version of [mem]; return true if {% \gamma(\{a\}) \cap \gamma(aps) != \{\} %}.
       note: this is worst-case linear in the size of the set *)
 
   val add : AccessPath.Abs.t -> astate -> astate
diff --git a/infer/src/clang/cTL.mli b/infer/src/clang/cTL.mli
index 392840758..452a84169 100644
--- a/infer/src/clang/cTL.mli
+++ b/infer/src/clang/cTL.mli
@@ -63,7 +63,7 @@ type t =
                                    there exists a node defining a super class in the hierarchy of the class
                                    defined by the current node (if any) where  phi holds *)
   | ET of ALVar.alexp list * transitions option * t
-      (** ET[T][l] phi <=> there exists a descentant an of the current node such that an is of type in set T
+      (** ET [T] [l] phi <=> there exists a descentant an of the current node such that an is of type in set T
           making a transition to a node an' via label l, such that in an phi holds. *)
   | InObjCClass of t * t
 [@@deriving compare]
diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli
index f04d97d2c..ea51ddfd8 100644
--- a/infer/src/concurrency/RacerDDomain.mli
+++ b/infer/src/concurrency/RacerDDomain.mli
@@ -73,7 +73,7 @@ module ThreadsDomain : sig
         etc.) *)
     | AnyThreadButSelf
         (** Current thread can run in parallel with other threads, but not with a copy of itself.
-        (concretization : \{ t | t \in TIDs ^ t != t_cur \} ) *)
+        (concretization : {% \{ t | t \in TIDs ^ t != t_cur \} %} ) *)
     | AnyThread
         (** Current thread can run in parallel with any thread, including itself (concretization:
             set of all TIDs ) *)