{"push_id":874287778,"size":2,"distinct_size":2,"ref":"refs/heads/master","head":"98e3c9a2f7aec9bd39e5a1c7064c84bf5045cc0a","before":"fd7458750d65d640951c979646f50c7f773031c6","commits":[{"sha":"019df74e404b47f3717903f397c0de23bb3718f4","author":{"email":"9964fcf15cf03644571918538e83618148b6cc34@princeton.edu","name":"Andrew W. Appel"},"message":"1. forward_call no longer takes an intro_pattern.  Instead,\nif your postcondition has an EX in it, you use the Intros tactic\nexplicitly after doing forward_call.\n\n2. Intros still moves propositions from the PROP clause above\nthe line, as before.  But if that proposition is of the form\n(x=E), then until now it would automatically do the substitution;\nnow you must do \"subst\" manually.\n\n3. start_function no longer does a \"simpl\" that affects your\nfunction specifications.  Instead, it leaves your funspecs alone,\npreserving them unsimplified.\n\nThe progs and sha proofs are brought up to date, but not other\nproofs (including hmac).","distinct":true,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/019df74e404b47f3717903f397c0de23bb3718f4"},{"sha":"98e3c9a2f7aec9bd39e5a1c7064c84bf5045cc0a","author":{"email":"9964fcf15cf03644571918538e83618148b6cc34@princeton.edu","name":"Andrew W. Appel"},"message":"Merge branch 'master' of github.com:PrincetonUniversity/VST","distinct":true,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/98e3c9a2f7aec9bd39e5a1c7064c84bf5045cc0a"}]}