Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Library Ltac2.Evar
Require
Import
Ltac2.Init
.
Ltac
2
Type
t
:=
evar
.
Ltac
2 @
external
equal
:
t
->
t
->
bool
:= "ltac2" "evar_equal".
Navigation
Standard Library
Table of contents
Index