Skip to content

`iEval ... in ...` for performing a tactic in an invidual proofmode hypothesis

Robbert Krebbers requested to merge robbert/iEval into master

This fixes issue #116 (closed).

This should work for tactics like simpl and (setoid) rewrite.

Edited by Robbert Krebbers

Merge request reports