Commit d0429c02 authored by Ralf Jung's avatar Ralf Jung

update opam file and README

parent 08f2cf2f
......@@ -2,7 +2,7 @@
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.
8.12 and later. Use the `v8.11` branch for a version that works with Coq 8.11.
## Installation
......
......@@ -13,7 +13,7 @@ This package implements string_to_ident in Ltac2, enabling support for Gallina n
"""
depends: [
"coq" {>= "8.11"}
"coq" {>= "8.12"}
"coq-iris" {>= "dev.2020-04-07.0.86b62616" | (>= "3.3.0" & < "4.0") | = "dev"}
]
......
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