data_at's definition is modified.
Minor improvements to forward_call, forward_if; minor cleanup of SHA proofs
Added a CompCert file that is imported by LinearizproofEFF.v
Whitespace cleanup
Make sure holes is executed as a bash script
Add missing reach.v to SEPCOMP_FILES
Remove after_at_external_excl clause from CoreSemantics interface.
Also, move a couple defns. from core_semantics.v to mem_lemmas.v.
Split Compositional CompCert files into a new directory, compcomp.
Now sepcomp contains mostly just CompCert-independent stuff.
Move sepcomp README to compcomp.
Add new README stub to sepcomp.
A new data_at is used. Previous examples in progs can work well now. nest2 is a new example. It is similar with nest3 but shows more details about alignments.
Greatly simplify the saturate_local tactic, make some adjustments to the entailer tactic
field_offset_unroll is changed into more generalized form for further use.
Substantial changes to the "saturate_local" and "entailer" tactics
to make them more efficient.

saturate_local:  more use of computational reflection, based on
   reified type environments (see the "findvars" tactic)
entailer, entailer! : much less use of "normalize", several other
 efficiency improvements.
1) Move Coresem.t typeclass from sepcomp/core_semantics.v
into linking/core_semantics_lemmas.v

2) Move core semantics lemmas into a new file.  Now,
sepcomp/core_semantics.v contains just the spec. of core semantics.
Several little things:
1. Remove some unnecessary calls to identity function (id) in data_at'.
2. Add the "TIMINGS=true" option to the Makefile, to collect timings
   into a "timings" file.   (See also util/format-timings)
3. Improve the "warn" facility in forward.v, to make the warning
  appear below the line instead of above the line, where it gets lost.
4. New "entailer_for_return" used by forward_return,
   does things specialized for the entailer after a return statement.
5. New "after_call" tactic, that cleans things up after a forward_call.
  This can't be done eagerly, because it must wait until the user
  (interactively) does proof steps that instantiate the Frame.
Improvements to forward_call, and related normalization rewrite rules
Some adjustments:
Make "align" and "Z.max" simplify, using Arguments command.
Rewrite "refold_andp" in the norm Hint database.
Tiny adjustment semax_store_field_nth will avoid the need
to fold with a t_struct_whatever during user proofs.
Split verif_sha_bdo into two files (bdo8 and bdo).
is_prop_lemma is added. The definitions and lemmas inside will be helpful to proving properties about lseg.
mapsto (in veric) now requires that the type is not volatile
computation_prover working. Now can take a user argument to tell it what user functions it should compute on

wrote and proved some functions for modifying reified entailments before sending them to mirror_shard. Changes goals like
!!(A/\B) && C |-- D into
!!A * !!B * C |-- D