Revise Haddocks for Crucible backends

The fact that these backends use an `AssumptionStack` is an
implementation detail that is not exposed via their interface, instead
clients interact with `getProofObligations`.

Also, point to a module that helps with dispatching such obligations.

crucible/src/Lang/Crucible/Backend.hs

@@ -16,13 +16,11 @@ offline solver connection, while the
 'Lang.Crucible.Backend.Online.OnlineBackend' is designed to be used with an
 online solver.
 
-The 'AS.AssumptionStack' tracks the assumptions that are in scope for each
-assertion, accounting for the branching and merging structure of programs.  The
-symbolic simulator manages the 'AS.AssumptionStack'. After symbolic simulation
-completes, the caller should traverse the 'AS.AssumptionStack' (or use
-combinators like 'AS.proofGoalsToList') to discharge the resulting proof
-obligations with a solver backend.
-
+The backend tracks the assumptions that are in scope for each assertion,
+accounting for the branching and merging structure of programs. After
+symbolic simulation completes, the caller should traverse the collected
+'ProofObligations'  (via 'getProofObligations') to discharge the resulting proof
+obligations with a solver backend. See also "Lang.Crucible.Backend.Prove".
 -}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}