Kill off last uses of "opaque type" (#4916)

### Description
<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->
<!-- Is this a bug fix for an issue visible in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: Sean McLaughlin <[email protected]>

docs/DafnyRef/Types.md

@@ -49,7 +49,7 @@ Dafny supports both reference types that contain the special `null` value
 
 A _Named Type_ is used to specify a user-defined type by a (possibly module- or class-qualified) name.
 Named types are introduced by
-class, trait, inductive, coinductive, synonym and opaque
+class, trait, inductive, coinductive, synonym and abstract
 type declarations. They are also used to refer to type variables.
 A Named Type is denoted by a dot-separated sequence of name segments ([Section 9.32](#sec-name-segment)).
 
@@ -1430,7 +1430,7 @@ type Y<T> = G
 ```
 declares `Y<T>` to be a synonym for the type `G`.
 If the `= G` is omitted then the declaration just declares a name as an uninterpreted
-_opaque_ type, as described in [Section 5.6.2](#sec-abstract-types).  Such types may be
+_abstract_ type, as described in [Section 5.6.2](#sec-abstract-types).  Such types may be
 given a definition elsewhere in the Dafny program.
 
   Here, `T` is a

docs/DafnyRef/UserGuide.md

@@ -1657,7 +1657,7 @@ the set of allowed identifiers) vary between languages, Dafny allows
 additional forms for the `{:extern}` attribute.
 
 The form `{:extern <s1>}` instructs `dafny` to compile references to most
-declarations using the name `s1` instead of the Dafny name. For [opaque
+declarations using the name `s1` instead of the Dafny name. For [abstract
 types](#sec-abstract-types), however, `s1` is sometimes used as a hint as
 to how to declare that type when compiling. This hint is interpreted
 differently by each compiler.