package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Tacinterp.Register`Source

Sourcetype ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t

val register_interp0 : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  ('glb, 'top) interp_fun ->
  unit