-
Robbert Krebbers authored
It is now able to destruct: - [own γ (a1 ⋅ a1)] into [own γ a1] and [own γ a2] - [own γ a] into [own γ a] and [own γ a] if [a] is persistent - [own γ (a,b)] by proceeding recursively. - [own γ (Some a)] by preceeding resursively.
39fe55fe
| Name |
Last commit
|
Last update |
|---|---|---|
| .. | ||
| coq_tactics.v | ||
| environments.v | ||
| ghost_ownership.v | ||
| intro_patterns.v | ||
| invariants.v | ||
| notation.v | ||
| pviewshifts.v | ||
| spec_patterns.v | ||
| sts.v | ||
| tactics.v | ||
| weakestpre.v |