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