You can search for identifiers within the package.
in-package search v0.2.0
rocq-runtime.vernac
Vernacstate.System
val protect : ('a -> 'b) -> 'a -> 'b
protect f x runs f x and discards changes in the system state (both Synterp.t and Interp.System.t). It doesn't touch the proof functional state in Interp.t
protect f x
f x
Synterp.t
Interp.System.t
Interp.t