• Robbert Krebbers's avatar
    Some refactoring of the proofmode proofs. · 2cec343c
    Robbert Krebbers authored
    I have introduced the following definition to avoid many case
    analyses where both branches had nearly identical proofs.
    
    Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
      (if p then □ P else P)%I.
    2cec343c
Name
Last commit
Last update
..
coq_tactics.v Loading commit data...
environments.v Loading commit data...
ghost_ownership.v Loading commit data...
intro_patterns.v Loading commit data...
invariants.v Loading commit data...
notation.v Loading commit data...
pviewshifts.v Loading commit data...
spec_patterns.v Loading commit data...
sts.v Loading commit data...
tactics.v Loading commit data...
weakestpre.v Loading commit data...