Skip to content

Alternative take on making proof mode terms more compact.

Robbert Krebbers requested to merge ci/robbert/pm_faster_alt into master

This is an alternative to !224 (closed) by splitting up envs_lookup_delete premises into envs_lookup and envs_delete.

@jtassaro Could you rebase !224 (closed) so we can compare?

The following tactics involve some other tricks:

  • tac_assumption: uses a let binding for envs_delete since its result is used twice
  • tac_specialize: uses a let binding for envs_delete since its result is used twice
  • tac_specialize_assert: uses a conjunction, not sure if it's worth the extra bloat in the Ltac code to do something smarter here.
Edited by Robbert Krebbers

Merge request reports