Skip to content

GitLab

Merged
Created by Robbert Krebbers@robbertkrebbersMaintainer

Alternative take on making proof mode terms more compact.

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