package coq-ltac-iter

  1. Overview
  2. No Docs
Access hint databases from tactics

Install

Dune Dependency

Authors

Maintainers

Sources

v1.1.1.tar.gz
sha512=56e58404f44a4d3e24a8c7f1075d057c19e146bba095b9d3faeb782f4380e23fc3a1b8bfbc0ce8be97fa507df7170ad255f33f7c0109c144c763de0deed1df26

Description

Provides tactics for performing various forms of iteration over hypotheses, hint databases, and other collections.

Published: 03 Jun 2020

Dependencies (2)

  1. coq >= "8.9" & < "8.10~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None