package coq-libhyps

  1. Overview
  2. No Docs
Hypotheses manipulation library

Install

Dune Dependency

github.com Edit opam file Versions (11)

Authors

  1. P
    Pierre Courtieu

Maintainers

  1. P
    Pierre.Courtieu@lecnam.net

Sources

libhyps-2.0.7.tar.gz
sha512=80ce980d5f66feceb00a7c1e1d892fbc330dee78c9cd00a8d3bc53706ac90c325b3c48372e0607276c909a2c48df0bea10c6d128dac0562e84218e840fd56699

Description

This library defines a set of tactics to manipulate hypothesis individually or by group. In particular it allows applying a tactic on each hypothesis of a goal, or only on new hypothesis after some tactic. Examples of manipulations: automatic renaming, subst, revert, or any tactic expecting a hypothesis name as argument.

It DOES NOT provide ANYMORE the especialize tactic to ease forward reasoning by instantianting one, several or all premisses of a hypothesis. Ths is due to coq's specialize being less permissive about evars. This may be fixed in the future.

Tags

keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming category:Miscellaneous/Coq Extensions logpath:LibHyps date:2022-09-23

Published: 15 Dec 2023

Dependencies

None

Dev Dependencies (1)

  1. coq (>= "8.11" & < "8.19~") | (= "dev")

Used by (1)

  1. coq-hydra-battles >= "0.6"

Conflicts

None