solve_load_rule_evaluation @proj_reptype

[andrew-appel]

In Ltac solve_load_rule_evaluation, it might be a good idea to change,

change proj_reptype with proj_reptype'

into

change @proj_reptype with @proj_reptype'

in case the compspecs in the goal differs from the current default compspecs. But I'm not sure whether this is really useful, because perhaps the user should have just done change_compspecs before forward.

[andrew-appel]

I found a second instance where this is necessary. In this case I'm trying to prove a particular general-purpose Hoare triple (semax) usable in many different functycontexts and/or compspecs, etc. More evidence that this change is a good idea.

[andrew-appel]

And also, similarly: in solve_store_rule_evaluation, add an @ to the change command as in:

change (@upd_reptype cs t gfs h0 h1 = rhs);

[andrew-appel]

And similarly, in tactic SEP_field_at_strong_unify the cs argument should be made explicit:

  | |- @data_at_ ?cs ?sh ?t ?p = _ /\ _ =>
        change (@data_at_ cs sh t p) with (@data_at cs sh t (@default_val _ t) p);
         SEP_field_at_strong_unify' gfs