1 files changed, 0 insertions, 15 deletions
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.