Verified Commit b077370a authored by Tej Chajed's avatar Tej Chajed

Fix up mentions of v8.11

parent ba39ed08
......@@ -2,11 +2,11 @@
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.12 and later. Use the `v8.11` branch for a version that works with Coq 8.11.
8.11 and later.
## Installation
You can install the Coq 8.11 version of this "plugin" via opam. First add the
You can install a Coq 8.11 version of this "plugin" via opam. First add the
Iris opam repository:
```sh
......@@ -34,6 +34,6 @@ Proof.
Qed.
```
## Acknowledgements
## Acknowledgments
This implementation strategy was suggested by Robbert Krebbers.
......@@ -13,7 +13,7 @@ This package implements string_to_ident in Ltac2, enabling support for Gallina n
"""
depends: [
"coq" {>= "8.12"}
"coq" {>= "8.11"}
"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