[sledge] Comments

Reviewed By: ngorogiannis

Differential Revision: D20120267

fbshipit-source-id: 4ae78bec8

sledge/src/symbheap/equality.ml

@@ -156,8 +156,8 @@ end
 
 (** Theory Solver *)
 
-(* orient equations s.t. Var < Memory < Extract < Concat < others, then
+(** orient equations s.t. Var < Memory < Extract < Concat < others, then
-   using height of aggregate nesting, and then using Term.compare *)
+    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
+(** try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q]
-   most one maximal solvable subterm, [kill], where [fv kill ⊈ us]; solve [p
+    has at most one maximal solvable subterm, [kill], where
-   = q] for [kill]; extend subst mapping [kill] to the solution *)
+    [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 =