• Robbert Krebbers's avatar
    Use `notypeclasses refine` in `iPoseProof` helpers. · d5d02af5
    Robbert Krebbers authored
    Also, rewrite `iIntoEmpValid`. Now, instead of using Ltac to traverse
    the type of the term and generate goals for the premises, we repeatedly
    apply a series of lemmas. This has the advantage that it works up to
    convertability, and we no longer need the `eval ...` hacks.
    d5d02af5
Name
Last commit
Last update
..
algebra.ref Loading commit data...
algebra.v Loading commit data...
atomic.ref Loading commit data...
atomic.v Loading commit data...
heap_lang.ref Loading commit data...
heap_lang.v Loading commit data...
heap_lang2.ref Loading commit data...
heap_lang2.v Loading commit data...
heap_lang_proph.ref Loading commit data...
heap_lang_proph.v Loading commit data...
ipm_paper.ref Loading commit data...
ipm_paper.v Loading commit data...
list_reverse.8.9.ref Loading commit data...
list_reverse.ref Loading commit data...
list_reverse.v Loading commit data...
mosel_paper.ref Loading commit data...
mosel_paper.v Loading commit data...
one_shot.ref Loading commit data...
one_shot.v Loading commit data...
one_shot_once.ref Loading commit data...
one_shot_once.v Loading commit data...
proofmode.ref Loading commit data...
proofmode.v Loading commit data...
proofmode_iris.ref Loading commit data...
proofmode_iris.v Loading commit data...
proofmode_monpred.ref Loading commit data...
proofmode_monpred.v Loading commit data...
telescopes.ref Loading commit data...
telescopes.v Loading commit data...
tree_sum.ref Loading commit data...
tree_sum.v Loading commit data...