Verified Commit 98e342b6 authored by Tej Chajed's avatar Tej Chajed

Add opam instructions

parent adc28e0f
......@@ -4,6 +4,16 @@ 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.
## Installation
You can install this "plugin" via opam. First add the Iris opam repository:
opam repo add iris-dev
Then install with `opam install coq-string-ident`.
Please register or sign in to reply
## Usage
Simply require this file before using the feature in the proof mode:
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