`Env`#

Ltac2.Env

val get : Libnames.full_path -> reference

get path returns the global reference corresponding to the absolute name given as argument.

raises Not_found
If the path does not correspond to a reference.

val path : reference -> Libnames.full_path

path ref returns the absolute name of the given reference.

raises Not_found
If the reference does not exist.

val expand : Libnames.qualid -> reference list

expand qualid returns the list of all global references whose absolute name contains the argument list as a suffix.

val instantiate :
  Environ.env ->
  Evd.evar_map ->
  reference ->
  Evd.evar_map * constr

instantiate env sigma ref returns a fresh instance of the corresponding reference, in particular generating fresh universe variables and constraints when this reference is universe-polymorphic.

Env#

`Env`#