From 968c13d056636239ffd41e8dfe2d049598836383 Mon Sep 17 00:00:00 2001
From: Sean McLaughlin <seanmcl@gmail.com>
Date: Tue, 26 Dec 2023 10:42:09 -0800
Subject: [PATCH] Kill off last uses of "opaque type" (#4916)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

### 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 <seanmcl@amazon.com>
---
 docs/DafnyRef/Types.md     | 4 ++--
 docs/DafnyRef/UserGuide.md | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md
index 27c90a90fe1..f31e9e8961d 100644
--- a/docs/DafnyRef/Types.md
+++ b/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
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index c361c47fe27..3cfc0555a4d 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/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.