Commit 4e574119 authored by Ralf Jung's avatar Ralf Jung

slightly expand README

parent 7d350b66
# Ltac2 implementation of `string_to_ident`
Implements `string_to_ident` using Ltac2, providing support for Gallina names in
Iris intro patterns on Coq 8.11 and later.
This "Iris plugin" implements the `string_to_ident` hook of the Iris proof mode
using Ltac2, providing support for Gallina names in Iris intro patterns on Coq
8.11 and later.
## Usage
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment