diff --git a/compiler/rustc_infer/src/infer/region_constraints/mod.rs b/compiler/rustc_infer/src/infer/region_constraints/mod.rs
index f93c9a31be6..19f83e3377a 100644
--- a/compiler/rustc_infer/src/infer/region_constraints/mod.rs
+++ b/compiler/rustc_infer/src/infer/region_constraints/mod.rs
@@ -190,44 +190,7 @@ pub enum GenericKind<'tcx> {
 /// This is described with an `AnyRegion('a, 'b)` node.
 #[derive(Debug, Clone)]
 pub enum VerifyBound<'tcx> {
-    /// This is a "conditional bound" that checks the result of inference
-    /// and supplies a bound if it ended up being relevant. It's used in situations
-    /// like this:
-    ///
-    /// ```rust
-    /// fn foo<'a, 'b, T: SomeTrait<'a>>
-    /// where
-    ///    <T as SomeTrait<'a>>::Item: 'b
-    /// ```
-    ///
-    /// If we have an obligation like `<T as SomeTrait<'?x>>::Item: 'c`, then
-    /// we don't know yet whether it suffices to show that `'b: 'c`. If `'?x` winds
-    /// up being equal to `'a`, then the where-clauses on function applies, and
-    /// in that case we can show `'b: 'c`. But if `'?x` winds up being something
-    /// else, the bound isn't relevant.
-    ///
-    /// More abstractly, this function takes a `Binder<VerifyIfEq>`. The binder
-    /// represents an existential binder -- i.e., if you have something like
-    ///
-    /// ```rust
-    /// where for<'a> <T as SomeTrait<'a>::Item: 'a
-    /// ```
-    ///
-    /// then the `for<'a>` corresponds to the binder. The idea is that we have
-    /// to find some instantiation of `'a` that can make `<T as SomeTrait<'a>>::Item`
-    /// equal to the final value of `G`, the generic we are checking.
-    ///
-    /// ```ignore (pseudo-rust)
-    /// fn(min) -> bool {
-    ///     exists<'a> {
-    ///         if G == K {
-    ///             B(min)
-    ///         } else {
-    ///             false
-    ///         }
-    ///     }
-    /// }
-    /// ```
+    /// See [`VerifyIfEq`] docs
     IfEq(ty::Binder<'tcx, VerifyIfEq<'tcx>>),
 
     /// Given a region `R`, expands to the function:
@@ -271,40 +234,44 @@ pub enum VerifyBound<'tcx> {
     AllBounds(Vec<VerifyBound<'tcx>>),
 }
 
-/// Given a kind K and a bound B, expands to a function like the
-/// following, where `G` is the generic for which this verify
-/// bound was created:
+/// This is a "conditional bound" that checks the result of inference
+/// and supplies a bound if it ended up being relevant. It's used in situations
+/// like this:
+///
+/// ```rust
+/// fn foo<'a, 'b, T: SomeTrait<'a>>
+/// where
+///    <T as SomeTrait<'a>>::Item: 'b
+/// ```
+///
+/// If we have an obligation like `<T as SomeTrait<'?x>>::Item: 'c`, then
+/// we don't know yet whether it suffices to show that `'b: 'c`. If `'?x` winds
+/// up being equal to `'a`, then the where-clauses on function applies, and
+/// in that case we can show `'b: 'c`. But if `'?x` winds up being something
+/// else, the bound isn't relevant.
+///
+/// In the [`VerifyBound`], this struct is enclosed in `Binder to account
+/// for cases like
+///
+/// ```rust
+/// where for<'a> <T as SomeTrait<'a>::Item: 'a
+/// ```
+///
+/// The idea is that we have to find some instantiation of `'a` that can
+/// make `<T as SomeTrait<'a>>::Item` equal to the final value of `G`,
+/// the generic we are checking.
 ///
 /// ```ignore (pseudo-rust)
 /// fn(min) -> bool {
-///     if G == K {
-///         B(min)
-///     } else {
-///         false
+///     exists<'a> {
+///         if G == K {
+///             B(min)
+///         } else {
+///             false
+///         }
 ///     }
 /// }
 /// ```
-///
-/// In other words, if the generic `G` that we are checking is
-/// equal to `K`, then check the associated verify bound
-/// (otherwise, false).
-///
-/// This is used when we have something in the environment that
-/// may or may not be relevant, depending on the region inference
-/// results. For example, we may have `where <T as
-/// Trait<'a>>::Item: 'b` in our where-clauses. If we are
-/// generating the verify-bound for `<T as Trait<'0>>::Item`, then
-/// this where-clause is only relevant if `'0` winds up inferred
-/// to `'a`.
-///
-/// So we would compile to a verify-bound like
-///
-/// ```ignore (illustrative)
-/// IfEq(<T as Trait<'a>>::Item, AnyRegion('a))
-/// ```
-///
-/// meaning, if the subject G is equal to `<T as Trait<'a>>::Item`
-/// (after inference), and `'a: min`, then `G: min`.
 #[derive(Debug, Copy, Clone, TypeFoldable)]
 pub struct VerifyIfEq<'tcx> {
     /// Type which must match the generic `G`