Adapt to coq/coq#19530

whonore · Sep 13, 2024 · f9e1fd7 · f9e1fd7
1 parent c1ae5b3
commit f9e1fd7
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/tests/coq/test_coqtop.py b/tests/coq/test_coqtop.py
@@ -135,9 +135,13 @@ def test_dispatch_unicode(coq: Coqtop) -> None:
 
 def test_dispatch_unprintable(coq: Coqtop) -> None:
     """Should be able to handle unprintable characters."""
-    succ, _, _, _ = coq.dispatch("Require Import String.")
+    succ, _, _, _ = coq.dispatch("Definition parse (x : Byte.byte) : option nat := None.")
     assert succ
-    succ, out, _, _ = coq.dispatch("Compute String (Ascii.ascii_of_nat 0) EmptyString.")
+    succ, _, _, _ = coq.dispatch("Definition print (x : nat) : list Byte.byte := cons Byte.x00 nil.")
+    assert succ
+    succ, _, _, _ = coq.dispatch("String Notation nat parse print : nat_scope.")
+    assert succ
+    succ, out, _, _ = coq.dispatch("Check O.")
     assert succ
     assert "\\x00" in out