diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index a483e513b..21892fb8e 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -156,8 +156,8 @@ end
 
 (** Theory Solver *)
 
-(* orient equations s.t. Var < Memory < Extract < Concat < others, then
-   using height of aggregate nesting, and then using Term.compare *)
+(** orient equations s.t. Var < Memory < Extract < Concat < others, then
+    using height of aggregate nesting, and then using Term.compare *)
 let orient e f =
   let compare e f =
     let rank e =
@@ -681,9 +681,10 @@ let subst_invariant us s0 s =
 
 type 'a zom = Zero | One of 'a | Many
 
-(* try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q] has at
-   most one maximal solvable subterm, [kill], where [fv kill ⊈ us]; solve [p
-   = q] for [kill]; extend subst mapping [kill] to the solution *)
+(** try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q]
+    has at most one maximal solvable subterm, [kill], where
+    [fv kill ⊈ us]; solve [p = q] for [kill]; extend subst mapping [kill]
+    to the solution *)
 let solve_poly_eq us p' q' subst =
   let diff = Term.sub p' q' in
   let max_solvables_not_ito_us =