In expr.v:
Generalize typecheck_temp_id to handle assignments  i:=e
where the type of e is Tarray(t), and the type of i is Tpointer(t).

Improvements in the cancellation tactic (fix some bugs regarding
frame inference, and better change lifts into backticks).

More progress on the SHA verification.


git-svn-id: https://svn.princeton.edu/appel/vst@5819 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
added reify_example.v, a file containing early attempts at reifying an entailment from entail_examples.v. This file has imports from mirror shard

git-svn-id: https://svn.princeton.edu/appel/vst@5820 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
saved progress before commit this time

git-svn-id: https://svn.princeton.edu/appel/vst@5821 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Lots more progress on the SHA256 proof,
along with more lemmas (and a bug-fix or two) in the floyd system.


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

git-svn-id: https://svn.princeton.edu/appel/vst@5823 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
implemented the mirror shard SepExpr module type. 

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