Learn
Platform
Packages
Community
Consortium
News
Learn
Platform
Packages
Community
Consortium
News
Get started
Core Library
Table of contents
Index
▾
Table of contents
Index
Library Ltac2.Evar
Require
Import
Ltac2.Init
.
Ltac
2
Type
t
:=
evar
.
Ltac
2 @
external
equal
:
t
->
t
->
bool
:= "rocq-runtime.plugins.ltac2" "evar_equal".