package coq-iris-string-ident
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Add support for Gallina names in intro patterns to the Iris Proof Mode
Install
Dune Dependency
Authors
Maintainers
Sources
string-ident-v0.1.0.tar.gz
sha512=af7b009914cb0f3d3cb336bed5968916a5b9cee527c6a60a558e5e0c1919f182112937762aad7419fd62fbb0e624fb886e3f5fc419da7563a717d6412289f974
Description
This package implements string_to_ident in Ltac2, enabling support for Gallina names in Iris intro patterns (within strings).
Tags
category:Miscellaneous/Coq Extensions keyword:iris logpath:iris_string_identPublished: 23 Jul 2020
On This Page