diff --git a/src/glossary.md b/src/glossary.md
index 36c0c9314..65b1978d0 100644
--- a/src/glossary.md
+++ b/src/glossary.md
@@ -30,6 +30,14 @@ items are defined in [implementations] and declared in [traits]. Only
 functions, constants, and type aliases can be associated. Contrast to a [free
 item].
 
+### Blanket implementation
+
+Any implementation where a type appears [uncovered](#uncovered-type). `impl<T> Foo
+for T`, `impl<T> Bar<T> for T`, `impl<T> Bar<Vec<T>> for T`, and `impl<T> Bar<T>
+for Vec<T>` are considered blanket impls. However, `impl<T> Bar<Vec<T>> for
+Vec<T>` is not a blanket impl, as all instances of `T` which appear in this `impl`
+are covered by `Vec`.
+
 ### Bound
 
 Bounds are constraints on a type or trait. For example, if a bound
@@ -65,6 +73,21 @@ For example, `2 + (3 * 4)` is an expression that returns the value 14.
 An [item] that is not a member of an [implementation], such as a *free
 function* or a *free const*. Contrast to an [associated item].
 
+### Fundamental traits
+
+A fundamental trait is one where adding an impl of it for an existing type is a breaking change. 
+The `Fn` traits and `Sized` are fundamental.
+
+### Fundamental type constructors
+
+A fundamental type constructor is a type where implementing a [blanket implementation](#blanket-implementation) over it 
+is a breaking change. `&`, `&mut`, `Box`, and `Pin`  are fundamental. 
+
+Any time a type `T` is considered [local](#local-type), `&T`, `&mut T`, `Box<T>`, and `Pin<T>` 
+are also considered local. Fundamental type constructors cannot [cover](#uncovered-type) other types. 
+Any time the term "covered type" is used, 
+the `T` in `&T`, `&mut T`, `Box<T>`, and `Pin<T>` is not considered covered.
+
 ### Inhabited
 
 A type is inhabited if it has constructors and therefore can be instantiated. An inhabited type is
@@ -87,6 +110,19 @@ A variable is initialized if it has been assigned a value and hasn't since been
 moved from. All other memory locations are assumed to be uninitialized. Only
 unsafe Rust can create such a memory without initializing it.
 
+### Local trait
+
+A `trait` which was defined in the current crate. A trait definition is local
+or not independent of applied type arguments. Given `trait Foo<T, U>`,
+`Foo` is always local, regardless of the types substituted for `T` and `U`.
+
+### Local type
+
+A `struct`, `enum`, or `union` which was defined in the current crate.
+This is not affected by applied type arguments. `struct Foo` is considered local, but
+`Vec<Foo>` is not. `LocalType<ForeignType>` is local. Type aliases do not 
+affect locality.
+
 ### Nominal types
 
 Types that can be referred to by a path directly. Specifically [enums],
@@ -158,6 +194,12 @@ It allows a type to make certain promises about its behavior.
 
 Generic functions and generic structs can use traits to constrain, or bound, the types they accept.
 
+### Uncovered type
+
+A type which does not appear as an argument to another type. For example,
+`T` is uncovered, but the `T` in `Vec<T>` is covered. This is only relevant for
+type arguments.
+
 ### Undefined behavior
 
 Compile-time or run-time behavior that is not specified. This may result in,
diff --git a/src/items/implementations.md b/src/items/implementations.md
index fedc4c18c..c4e63b2fa 100644
--- a/src/items/implementations.md
+++ b/src/items/implementations.md
@@ -152,7 +152,7 @@ impl Shape for Circle {
 
 ### Trait Implementation Coherence
 
-A trait implementation is considered incoherent if either the orphan check fails
+A trait implementation is considered incoherent if either the orphan rules check fails
 or there are overlapping implementation instances.
 
 Two trait implementations overlap when there is a non-empty intersection of the
@@ -160,21 +160,23 @@ traits the implementation is for, the implementations can be instantiated with
 the same type. <!-- This is probably wrong? Source: No two implementations can
 be instantiable with the same set of types for the input type parameters. -->
 
-The `Orphan Check` states that every trait implementation must meet either of
-the following conditions:
+#### Orphan rules
 
-1.  The trait being implemented is defined in the same crate.
+Given `impl<P1..=Pn> Trait<T1..=Tn> for T0`, an `impl` is valid only if at
+least one of the following is true:
 
-2.  At least one of either `Self` or a generic type parameter of the trait must
-    meet the following grammar, where `C` is a nominal type defined
-    within the containing crate:
+- `Trait` is a [local trait]
+- All of
+  - At least one of the types `T0..=Tn` must be a [local type]. Let `Ti` be the
+    first such type.
+  - No [uncovered type] parameters `P1..=Pn` may appear in `T0..Ti` (excluding
+    `Ti`)
+
+Only the appearance of *uncovered* type parameters is restricted.
+Note that for the purposes of coherence, [fundamental types] are
+special. The `T` in `Box<T>` is not considered covered, and `Box<LocalType>` 
+is considered local.
 
-    ```ignore
-     T = C
-       | &C
-       | &mut C
-       | Box<C>
-    ```
 
 ## Generic Implementations
 
@@ -224,3 +226,7 @@ attributes].
 [path]: ../paths.md
 [the lint check attributes]: ../attributes/diagnostics.md#lint-check-attributes
 [Unsafe traits]: traits.md#unsafe-traits
+[local trait]: ../glossary.md#local-trait
+[local type]: ../glossary.md#local-type
+[fundamental types]: ../glossary.md#fundamental-type-constructors
+[uncovered type]: ../glossary.md#uncovered-type