Library Ltac2.Env


From Ltac2 Require Import Init Std.

Ltac2 @ external get : ident list -> Std.reference option := "coq-core.plugins.ltac2" "env_get".
Returns the global reference corresponding to the absolute name given as argument if it exists.

Ltac2 @ external expand : ident list -> Std.reference list := "coq-core.plugins.ltac2" "env_expand".
Returns the list of all global references whose absolute name contains the argument list as a suffix.

Ltac2 @ external path : Std.reference -> ident list := "coq-core.plugins.ltac2" "env_path".
Returns the absolute name of the given reference. Panics if the reference does not exist.

Ltac2 @ external instantiate : Std.reference -> constr := "coq-core.plugins.ltac2" "env_instantiate".
Returns a fresh instance of the corresponding reference, in particular generating fresh universe variables and constraints when this reference is universe-polymorphic.