From e2bea22f6ca580ad74ab86d02da2c444aa2352e9 Mon Sep 17 00:00:00 2001
From: texastony <5892063+texastony@users.noreply.github.com>
Date: Wed, 27 Jul 2022 15:29:59 -0500
Subject: [PATCH 1/3] chore: address dafny-lang/dafny#2500

---
 .github/PULL_REQUEST_TEMPLATE.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index c23fc89fd..5859885dc 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -6,3 +6,17 @@
 
 
 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
+
+# Due to [dafny-lang/dafny#2500](https://github.com/dafny-lang/dafny/issues/2500), Traits are dangerous:
+1. [ ] Does this PR add any traits or classes that extend a trait?
+2. [ ] Are these traits annoated with `{:termination false}`?
+
+The override checks on the specifications on a class' functions/methods/etc. 
+validating that specifcations are 
+at least as strong as those on the traits it implements
+are not working correctly when 
+that trait is defined in a different module 
+(and hence must have `{:termination false}` on it).
+
+As such, if either (1.) or (2.) is true:
+Have you [ ] manually verified all the trait specifications are copied onto classes that extend them?

From 588a7740aee78e0e679fa0a84b4db7d3e2493689 Mon Sep 17 00:00:00 2001
From: texastony <5892063+texastony@users.noreply.github.com>
Date: Wed, 27 Jul 2022 15:34:04 -0500
Subject: [PATCH 2/3] fix: typos and formatting

---
 .github/PULL_REQUEST_TEMPLATE.md | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 5859885dc..4d7a82af8 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -9,11 +9,14 @@ By submitting this pull request, I confirm that my contribution is made under th
 
 # Due to [dafny-lang/dafny#2500](https://github.com/dafny-lang/dafny/issues/2500), Traits are dangerous:
 1. [ ] Does this PR add any traits or classes that extend a trait?
-2. [ ] Are these traits annoated with `{:termination false}`?
+2. [ ] Are these traits annotated with `{:termination false}`?
 
-The override checks on the specifications on a class' functions/methods/etc. 
-validating that specifcations are 
-at least as strong as those on the traits it implements
+The override checks on 
+the specifications on
+a class' functions/methods/etc. validating
+that specifications are 
+at least as strong as those on
+the traits it implements
 are not working correctly when 
 that trait is defined in a different module 
 (and hence must have `{:termination false}` on it).

From 5b0d1a984b1fb5b51a997e0c844fdeb691cb5aca Mon Sep 17 00:00:00 2001
From: texastony <5892063+texastony@users.noreply.github.com>
Date: Wed, 27 Jul 2022 15:43:49 -0500
Subject: [PATCH 3/3] fix: formatting

---
 .github/PULL_REQUEST_TEMPLATE.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
index 4d7a82af8..8427e3636 100644
--- a/.github/PULL_REQUEST_TEMPLATE.md
+++ b/.github/PULL_REQUEST_TEMPLATE.md
@@ -22,4 +22,4 @@ that trait is defined in a different module
 (and hence must have `{:termination false}` on it).
 
 As such, if either (1.) or (2.) is true:
-Have you [ ] manually verified all the trait specifications are copied onto classes that extend them?
+- [ ] manually verified all the trait specifications are copied onto classes that extend them?