Refactor head_inv/tail_inv
Refactored functions for a cleaner separation between computable and non-computable ones
Added support for equality to do_computation
Added do_computation to Makefile.
Instantiate Cancellation module in mirror_cancel.v. This contains the function that rewrites, proves Pure facts, and cancels
Slight polishing of corediagram rule: 
removal of the superfluous postconditions SM_wd and sm_valid
Coordination check-in
Reach-closed semantics (Lennart: this is the extended semantics we discussed last week)
Minor incidental cleanup
Push linking proof forward another inch
Add rc_semantics to linking target in Makefile
In R_inv (linking invariant), make mu_tot canonical by always restricting to the visible set.
Reformulate/clean up linking.v in preparation for branch to compcert_linking.v
Add compcert_linking.v, which specializes linking semantics to CompCert semantics (thought I could avoid branching linking.v/compcert_linking.v but it seems this is now unavoidable if we want to integrate rc_semantics)
Integrate rc_semantics into compcert_linking; some invariants in linking_proof.v still need to be updated.
Comments
Experimental simulation structure for equality passes, 
with transitivity proofs eq-eq and inj-eq.
tactics and lemmas for mirror-shard canceller