package coq-tactician-dummy

  1. Overview
  2. Homepage
A dummy implementation of Tactician

Install

Dune Dependency

Authors

Maintainers

Sources

1.0-beta1.tar.gz
sha512=99c2a46202263745fa509a5fcea4b8a09f0cfb5e268a5fa610e32731781a3235845d977e299d3a48c4f2a7b2e3cae0b2b415c7bc57f4b685e8da960a53ac40ca

Description

This package acts as a stand-in for the Tactician plugin (coq-tactician). It provides short files that replicate Tactician's tactics without actually doing much. This is useful when you have a development that uses Tactician that you want to package up. In most situations, it is not a good idea to have your package directly depend on coq-tactician. Instead you should load Tactician through your coqrc file. In order for your package to be compilable by others, your package can depend on this package. Just add From Tactician import Ltac1Dummy in your development and you are good to go.

Dependencies (2)

  1. dune >= "2.5"
  2. coq >= "8.6.1"

Dev Dependencies

None

Used by (1)

  1. coq-tactician < "1.0~beta2~neural+8.11"

Conflicts

None

Rocq

Interactive Theorem Prover