Library Ltac2.Constant
Require Import Ltac2.Init.
Ltac2 Type t :=
constant.
Ltac2 @
external equal :
constant ->
constant ->
bool := "rocq-runtime.plugins.ltac2" "constant_equal".
Constants obtained through module aliases or Include are not
considered equal by this function.
Ltac2 @external print : t -> message
:= "rocq-runtime.plugins.ltac2" "constant_print".
Print the constant using the shortest qualified identifier which refers to it.
Does not avoid variable names in the current or global environment.