Improved RelyGuarantee-Theorems by adding rule variant effect_diagram_strong_perm
The rule contains the assertion regarding permissions of locations in 
source-langguage effects, but imposes this condition in the lasues on E_Tgt.
Contrary to several alternatives, this rule is actually transitive.

Minor polishing elsewhere.

git-svn-id: https://svn.princeton.edu/appel/vst@5794 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Completed proof of Lemma sm_normalize_inject and moved it from
StructuredInjections.v to effect_simulations.v since it uses REACH.

git-svn-id: https://svn.princeton.edu/appel/vst@5795 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
1.  Remove the "Load loadpath" command from various progs/*.v files;
   it's obsolete.

2.  Tweaks to the go_lower0 tactic; but I'm not done tweaking this, just yet.
  The unrestricted "simpl" still has a habit of taking forever, sometimes.

3.  More progress on the correctness proof of sha256_block_data_order.


git-svn-id: https://svn.princeton.edu/appel/vst@5796 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
added _CoqProject file. Should start Coq with correct loadpath in Proof General.

git-svn-id: https://svn.princeton.edu/appel/vst@5797 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
In veric:
 new program-logic rules  semax_skip_seq, semax_seq_skip.

In floyd:  
 new derived rules  semax_frame_seq, semax_frame1.

In progs:
 More progress on verif_sha.


git-svn-id: https://svn.princeton.edu/appel/vst@5798 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
In client lemmas: minor fix to go_lower (restore the clearing
  of "rho" if it is not live).

In forward.v:  Major overhaul and cleanup of the tactics:
  forward, forward1, forward_with.


git-svn-id: https://svn.princeton.edu/appel/vst@5799 e2b0c78b-04ed-0310-b50c-832c51d4eb4a