4 files changed, 31 insertions, 19 deletions
diff --git a/test-suite/bugs/closed/bug_9684.v b/test-suite/bugs/closed/bug_9684.v
new file mode 100644
index 0000000000..436a00585b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9684.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record foo := mkFoo { proj1 : bool; proj2 : bool }.
+
+Definition x := mkFoo true false.
+Definition proj x := proj2 x.
+
+Lemma oops : proj = fun x => proj1 x.
+Proof. Fail native_compute; reflexivity. Abort.
+
+(*
+Lemma bad : False.
+assert (proj1 x = proj x).
+  rewrite oops; reflexivity.
+discriminate.
+Qed.
+
+Print Assumptions bad.
+*)
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index cb49e66ed7..460c77879c 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -82,10 +82,6 @@ function (of_uint) targets an option type.
 The command has indeed failed with message:
 The 'abstract after' directive has no effect when the parsing function
 (of_uint) targets an option type. [abstract-large-number-no-op,numbers]
-The command has indeed failed with message:
-The reference of_uint was not found in the current environment.
-The command has indeed failed with message:
-The reference of_uint was not found in the current environment.
 let v := of_uint (Decimal.D1 Decimal.Nil) in v : unit
      : unit
 let v := 0%test13 in v : unit
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index fcfdd82dcc..44805ad09d 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -207,21 +207,6 @@ Module Test10.
   Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
 End Test10.
 
-Module Test11.
-  (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
-  Inductive unit11 := tt11.
-  Declare Scope unit11_scope.
-  Delimit Scope unit11_scope with unit11.
-  Goal True.
-    evar (to_uint : unit11 -> Decimal.uint).
-    evar (of_uint : Decimal.uint -> unit11).
-    Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
-    exact I.
-    Unshelve.
-    all: solve [ constructor ].
-  Qed.
-End Test11.
-
 Module Test12.
   (* Test for numeral notations on context variables *)
   Declare Scope test12_scope.
diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v
new file mode 100644
index 0000000000..ea3907ef8a
--- /dev/null
+++ b/test-suite/success/NumeralNotationsNoLocal.v
@@ -0,0 +1,12 @@
+(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+Inductive unit11 := tt11.
+Declare Scope unit11_scope.
+Delimit Scope unit11_scope with unit11.
+Goal True.
+  evar (to_uint : unit11 -> Decimal.uint).
+  evar (of_uint : Decimal.uint -> unit11).
+  Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
+  exact I.
+  Unshelve.
+  all: solve [ constructor ].
+Qed.