[sledge] Improve Sh docs

Reviewed By: ngorogiannis

Differential Revision: D19221879

fbshipit-source-id: 5ef052877

sledge/src/symbheap/sh.mli

@@ -66,9 +66,9 @@ val and_cong : Equality.t -> t -> t
 
 val with_pure : Term.t list -> t -> t
 (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
-    [pure] are defined in the same vocabulary, induce the same congruence,
+    [pure] are defined in the same vocabulary. Note that [cong] is not
-    etc. It can essentially only be used when [pure] is logically equivalent
+    weakened, so if [pure] and [q.pure] do not induce the same congruence,
-    to [q.pure], but perhaps syntactically simpler. *)
+    then the result will have a stronger [cong] than induced by its [pure]. *)
 
 val rem_seg : seg -> t -> t
 (** [star (seg s) (rem_seg s q)] is equivalent to [q], assuming that [s] is
@@ -105,7 +105,7 @@ val extend_us : Var.Set.t -> t -> t
 (** Query *)
 
 val is_emp : t -> bool
-(** Holds of [emp]. *)
+(** Holds of [emp], with any vocabulary, existentials, and congruence. *)
 
 val is_false : t -> bool
 (** Holds only of inconsistent formulas, does not hold of all inconsistent