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.