Undeprecate inspect idiom (#2107)

Author: MatthewDaggitt

CHANGELOG.md

@@ -1556,14 +1556,6 @@ Deprecated names
 * This fixes the fact we had picked the wrong name originally. The erased modality
   corresponds to @0 whereas the irrelevance one corresponds to `.`.
 
-### Deprecated `Relation.Binary.PropositionalEquality.inspect`
-    in favour of `with ... in ...` syntax (issue #1580; PRs #1630, #1930)
-
-* In `Relation.Binary.PropositionalEquality`
-  both the record type `Reveal_·_is_`
-  and its principal mode of use, `inspect`,
-  have been deprecated in favour of the new `with ... in ...` syntax.
-  See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality)
 
 New modules
 -----------

src/Relation/Binary/PropositionalEquality.agda

@@ -104,15 +104,17 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where
   ≢-≟-identity = dec-no (x ≟ y)
 
 
+------------------------------------------------------------------------
+-- Inspect
 
+-- Inspect can be used when you want to pattern match on the result r
+-- of some expression e, and you also need to "remember" that r ≡ e.
 
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
+-- See README.Inspect for an explanation of how/why to use this.
 
--- Version 2.0
+-- Normally (but not always) the new `with ... in` syntax described at
+-- https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality
+-- can be used instead."
 
 record Reveal_·_is_ {A : Set a} {B : A → Set b}
                     (f : (x : A) → B x) (x : A) (y : B x) :
@@ -123,12 +125,3 @@ record Reveal_·_is_ {A : Set a} {B : A → Set b}
 inspect : ∀ {A : Set a} {B : A → Set b}
           (f : (x : A) → B x) (x : A) → Reveal f · x is f x
 inspect f x = [ refl ]
-
-{-# WARNING_ON_USAGE Reveal_·_is_
-"Warning: Reveal_·_is_ was deprecated in v2.0.
-Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead."
-#-}
-{-# WARNING_ON_USAGE inspect
-"Warning: inspect was deprecated in v2.0.
-Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead."
-#-}