Verified Commit 4410c1d3 authored by Tej Chajed's avatar Tej Chajed

Remove Ltac2 from the name

parent 85752806
opam-version: "2.0"
name: "coq-ltac2-string-ident"
name: "coq-string-ident"
maintainer: "Tej Chajed <tchajed@mit.edu>"
authors: "Tej Chajed <tchajed@mit.edu>"
license: "BSD-3-Clause"
homepage: "https://gitlab.mpi-sws.org/iris/ltac2-string-ident"
bug-reports: "https://gitlab.mpi-sws.org/iris/ltac2-string-ident/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/ltac2-string-ident.git"
homepage: "https://gitlab.mpi-sws.org/iris/string-ident"
bug-reports: "https://gitlab.mpi-sws.org/iris/string-ident/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/string-ident.git"
version: "dev"
synopsis: "Add support for Gallina names in intro patterns to the Iris Proof Mode"
......@@ -24,6 +24,5 @@ install: [make "install"]
tags: [
"category:Miscellaneous/Coq Extensions"
"keyword:iris"
"keyword:ltac2"
"logpath:IrisStringIdent"
]
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