diff --git a/src/borrow_check.md b/src/borrow_check.md
index 40858b1b4..b3eeaa387 100644
--- a/src/borrow_check.md
+++ b/src/borrow_check.md
@@ -51,13 +51,14 @@ the [`mir_borrowck`] query.
   the purpose of this type check is to determine all of the constraints between
   different regions.
 - Next, we do [region inference](borrow_check/region_inference.html), which computes
-  the values of each region — basically, points in the control-flow graph.
+  the values of each region — basically, the points in the control-flow graph where
+  each lifetime must be valid according to the constraints we collected.
 - At this point, we can compute the "borrows in scope" at each point.
 - Finally, we do a second walk over the MIR, looking at the actions it
   does and reporting errors. For example, if we see a statement like
   `*a + 1`, then we would check that the variable `a` is initialized
   and that it is not mutably borrowed, as either of those would
-  require an error to be reported.
-  - Doing this check requires the results of all the previous analyses.
+  require an error to be reported. Doing this check requires the results of all
+  the previous analyses.
 
 [`replace_regions_in_mir`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.replace_regions_in_mir.html
diff --git a/src/borrow_check/region_inference.md b/src/borrow_check/region_inference.md
index 95c2bc804..7fe50b870 100644
--- a/src/borrow_check/region_inference.md
+++ b/src/borrow_check/region_inference.md
@@ -9,7 +9,7 @@ deprecated once they become the standard kind of lifetime.)
 
 The MIR-based region analysis consists of two major functions:
 
-- `replace_regions_in_mir`, invoked first, has two jobs:
+- [`replace_regions_in_mir`], invoked first, has two jobs:
   - First, it finds the set of regions that appear within the
     signature of the function (e.g., `'a` in `fn foo<'a>(&'a u32) {
     ... }`). These are called the "universal" or "free" regions – in
@@ -21,49 +21,67 @@ The MIR-based region analysis consists of two major functions:
     not of much interest. The intention is that – eventually – they
     will be "erased regions" (i.e., no information at all), since we
     won't be doing lexical region inference at all.
-- `compute_regions`, invoked second: this is given as argument the
+- [`compute_regions`], invoked second: this is given as argument the
   results of move analysis. It has the job of computing values for all
   the inference variables that `replace_regions_in_mir` introduced.
-  - To do that, it first runs the [MIR type checker](#mirtypeck). This
+  - To do that, it first runs the [MIR type checker]. This
     is basically a normal type-checker but specialized to MIR, which
-    is much simpler than full Rust of course. Running the MIR type
+    is much simpler than full Rust, of course. Running the MIR type
     checker will however create **outlives constraints** between
     region variables (e.g., that one variable must outlive another
     one) to reflect the subtyping relationships that arise.
   - It also adds **liveness constraints** that arise from where variables
     are used.
-  - More details to come, though the [NLL RFC] also includes fairly thorough
-    (and hopefully readable) coverage.
+  - After this, we create a [`RegionInferenceContext`] with the constraints we
+    have computed and the inference variables we introduced and use the
+    [`solve`] method to infer values for all region inference varaibles.
+  - The [NLL RFC] also includes fairly thorough (and hopefully readable)
+    coverage.
 
 [fvb]: ../appendix/background.html#free-vs-bound
+[`replace_regions_in_mir`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.replace_regions_in_mir.html
+[`compute_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.compute_regions.html
+[`RegionInferenceContext`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html
+[`solve`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.solve
 [NLL RFC]: http://rust-lang.github.io/rfcs/2094-nll.html
+[MIR type checker]: ./type_check.md
 
 ## Universal regions
 
-*to be written* – explain the `UniversalRegions` type
+The [`UnversalRegions`] type represents a collection of _universal_ regions
+corresponding to some MIR `DefId`. It is constructed in
+[`replace_regions_in_mir`] when we replace all regions with fresh inference
+variables. [`UniversalRegions`] contains indices for all the free regions in
+the given MIR along with any relationships that are _known_ to hold between
+them (e.g. implied bounds, where clauses, etc.).
 
-## Region variables and constraints
+For example, given the MIR for the following function:
 
-*to be written* – describe the `RegionInferenceContext` and
-the role of `liveness_constraints` vs other `constraints`, plus
-
-## Closures
+```rust
+fn foo<'a>(x: &'a u32) {
+    // ...
+}
+```
 
-*to be written*
+we would create a universal region for `'a` and one for `'static`. There may
+also be some complications for handling closures, but we will ignore those for
+the moment.
 
-<a name="mirtypeck"></a>
+TODO: write about _how_ these regions are computed.
 
-## The MIR type-check
+[`UniversalRegions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/universal_regions/struct.UniversalRegions.html
 
-## Representing the "values" of a region variable
+## Region variables
 
-The value of a region can be thought of as a **set**; we call the
-domain of this set a `RegionElement`. In the code, the value for all
-regions is maintained in
-[the `rustc_mir::borrow_check::nll::region_infer` module][ri]. For
-each region we maintain a set storing what elements are present in its
-value (to make this efficient, we give each kind of element an index,
-the `RegionElementIndex`, and use sparse bitsets).
+The value of a region can be thought of as a **set**. This set contains all
+points in the MIR where the region is valid along with any regions that are
+outlived by this region (e.g. if `'a: 'b`, then `end('b)` is in the set for
+`'a`); we call the domain of this set a `RegionElement`. In the code, the value
+for all regions is maintained in [the
+`rustc_mir::borrow_check::nll::region_infer` module][ri]. For each region we
+maintain a set storing what elements are present in its value (to make this
+efficient, we give each kind of element an index, the `RegionElementIndex`, and
+use sparse bitsets).
 
 [ri]: https://github.com/rust-lang/rust/tree/master/src/librustc_mir/borrow_check/nll/region_infer/
 
@@ -83,12 +101,148 @@ The kinds of region elements are as follows:
   for details on placeholders, see the section
   [placeholders and universes](#placeholder).
 
-## Causal tracking
+## Constraints
+
+Before we can infer the value of regions, we need to collect constraints on the
+regions. There are two primary types of constraints.
+
+1. Outlives constraints. These are constraints that one region outlives another
+   (e.g. `'a: 'b`). Outlives constraints are generated by the [MIR type
+   checker].
+2. Liveness constraints. Each region needs to be live at points where it can be
+   used. These constraints are collected by [`generate_constraints`].
+
+[`generate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/constraint_generation/fn.generate_constraints.html
+
+## Inference Overview
+
+So how do we compute the contents of a region? This process is called _region
+inference_. The high-level idea is pretty simple, but there are some details we
+need to take care of.
+
+Here is the high-level idea: we start off each region with the MIR locations we
+know must be in it from the liveness constraints. From there, we use all of the
+outlives constraints computed from the type checker to _propagate_ the
+constraints: for each region `'a`, if `'a: 'b`, then we add all elements of
+`'b` to `'a`, including `end('b)`. This all happens in
+[`propagate_constraints`].
+
+Then, we will check for errors. We first check that type tests are satisfied by
+calling [`check_type_tests`]. This checks constraints like `T: 'a`. Second, we
+check that universal regions are not "too big". This is done by calling
+[`check_universal_regions`]. This checks that for each region `'a` if `'a`
+contains the element `end('b)`, then we must already know that `'a: 'b` holds
+(e.g. from a where clause). If we don't already know this, that is an error...
+well, almost. There is some special handling for closures that we will discuss
+later.
+
+### Example
+
+Consider the following example:
 
-*to be written* – describe how we can extend the values of a variable
- with causal tracking etc
+```rust,ignore
+fn foo<'a, 'b>(x: &'a usize) -> &'b usize {
+    x
+}
+```
+
+Clearly, this should not compile because we don't know if `'a` outlives `'b`
+(if it doesn't then the return value could be a dangling reference).
 
-<a name="placeholder"></a>
+Let's back up a bit. We need to introduce some free inference variables (as is
+done in [`replace_regions_in_mir`]). This example doesn't use the exact regions
+produced, but it (hopefully) is enough to get the idea across.
+
+```rust,ignore
+fn foo<'a, 'b>(x: &'a /* '#1 */ usize) -> &'b /* '#3 */ usize {
+    x // '#2, location L1
+}
+```
+
+Some notation: `'#1`, `'#3`, and `'#2` represent the universal regions for the
+argument, return value, and the expression `x`, respectively. Additionally, I
+will call the location of the expression `x` `L1`.
+
+So now we can use the liveness constraints to get the following starting points:
+
+Region  | Contents
+--------|----------
+'#1     |
+'#2     | `L1`
+'#3     | `L1`
+
+Now we use the outlives constraints to expand each region. Specifically, we
+know that `'#2: '#3` ...
+
+Region  | Contents
+--------|----------
+'#1     | `L1`
+'#2     | `L1, end('#3) // add contents of '#3 and end('#3)`
+'#3     | `L1`
+
+... and `'#1: '#2`, so ...
+
+Region  | Contents
+--------|----------
+'#1     | `L1, end('#2), end('#3) // add contents of '#2 and end('#2)`
+'#2     | `L1, end('#3)`
+'#3     | `L1`
+
+Now, we need to check that no regions were too big (we don't have any type
+tests to check in this case). Notice that `'#1` now contains `end('#3)`, but
+we have no `where` clause or implied bound to say that `'a: 'b`... that's an
+error!
+
+### Some details
+
+The [`RegionInferenceContext`] type contains all of the information needed to
+do inference, including the universal regions from [`replace_regions_in_mir`] and
+the constraints computed for each region. It is constructed just after we
+compute the liveness constraints.
+
+Here are some of the fields of the struct:
+
+- [`constraints`]: contains all the outlives constraints.
+- [`liveness_constraints`]: contains all the liveness constraints.
+- [`universal_regions`]: contains the `UniversalRegions` returned by
+  [`replace_regions_in_mir`].
+- [`universal_region_relations`]: contains relations known to be true about
+  universal regions. For example, if we have a where clause that `'a: 'b`, that
+  relation is assumed to be true while borrow checking the implementation (it
+  is checked at the caller), so `universal_region_relations` would contain `'a:
+  'b`.
+- [`type_tests`]: contains some constraints on types that we must check after
+  inference (e.g. `T: 'a`).
+- [`closure_bounds_mapping`]: used for propagating region constraints from
+  closures back out to the creater of the closure.
+
+[`constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.constraints
+[`liveness_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.liveness_constraints
+[`universal_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.universal_regions
+[`universal_region_relations`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.universal_region_relations
+[`type_tests`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.type_tests
+[`closure_bounds_mapping`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.closure_bounds_mapping
+
+TODO: should we discuss any of the others fields? What about the SCCs?
+
+Ok, now that we have constructed a `RegionInferenceContext`, we can do
+inference. This is done by calling the [`solve`] method on the context. This
+is where we call [`propagate_constraints`] and then check the resulting type
+tests and universal regions, as discussed above.
+
+[`propagate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.propagate_constraints
+[`check_type_tests`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_type_tests
+[`check_universal_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_universal_regions
+
+## Closures
+
+When we are checking the type tests and universal regions, we may come across a
+constraint that we can't prove yet if we are in a closure body! However, the
+necessary constraints may actually hold (we just don't know it yet). Thus, if
+we are inside a closure, we just collect all the constraints we can't prove yet
+and return them. Later, when we are borrow check the MIR node that created the
+closure, we can also check that these constraints hold. At that time, if we
+can't prove they hold, we report an error.
 
 ## Placeholders and universes
 
@@ -534,3 +688,6 @@ Now constraint propagation is done, but when we check the outlives
 relationships, we find that `V2` includes this new element `placeholder(1)`,
 so we report an error.
 
+## Borrow Checker Errors
+
+TODO: we should discuss how to generate errors from the results of these analyses.