Support explicit naming of hypotheses generated by funelim

mattam82 / Coq-Equations

A function definition package for Coq

http://mattam82.github.io/Coq-Equations

GNU Lesser General Public License v2.1

223 stars 44 forks source link

Support explicit naming of hypotheses generated by funelim #415

Open anton-trunov opened 3 years ago

anton-trunov commented 3 years ago

It would be great to have a variant of funelim like induction foo as [... | ... | ...] or better yet for compatibility with the Mathcomp style an option to not move everything into the context.

mattam82 commented 2 years ago

There is the apply_funelim tactic which does not introduce hypotheses.

Tuplanolla commented 2 years ago

The apply_funelim tactic should be mentioned in the reference manual.