package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Arguments_renaming`Source

Sourceval rename_arguments : bool -> Names.GlobRef.t -> Names.Name.t list -> unit

Sourceval arguments_names : Environ.env -> Names.GlobRef.t -> Names.Name.t list

Not_found is raised if no names are defined for r

val rename_type : 
  Environ.env ->
  Constr.types ->
  Names.GlobRef.t ->
  Constr.types

Sourceval rename_typing : Environ.env -> Constr.constr -> Environ.unsafe_judgment

Typechecks using the kernel Typeops.infer