Reset @Ident never errors (since implementation by stm instead of lib)

SkySkimmer · Dec 9, 2021 · ece5fe1 · ece5fe1
1 parent 3c90295
commit ece5fe1
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -733,9 +733,6 @@ interactively, they cannot be part of a Coq file loaded via
    declared object as well as the name of a section. One cannot reset
    over the name of a module or of an object inside a module.
 
-   .. exn:: @ident: no such entry.
-      :undocumented:
-
 .. cmd:: Reset Initial
 
    Goes back to the initial state, just after the start