{"push_id":1239584754,"size":3,"distinct_size":3,"ref":"refs/heads/master","head":"2041cb84726c840246da5d4ef18e6bc6d35dd8a7","before":"19e2860269bd44b59e6d35d19685c93b523585dc","commits":[{"sha":"03951a517ed63e315c016fe381742eff11508119","author":{"name":"Armael","email":"685e678634892b7d707059b1800da7ebe1b90d3d@ens-lyon.fr"},"message":"Simplify proofs of auxiliary lemmas in cfHeapsBaseScript","distinct":true,"url":"https://api.github.com/repos/CakeML/cakeml/commits/03951a517ed63e315c016fe381742eff11508119"},{"sha":"c266d00350134fd39fb83d596f29d574c9a05c12","author":{"name":"Armael","email":"685e678634892b7d707059b1800da7ebe1b90d3d@ens-lyon.fr"},"message":"Implement [xffi], and a few fixes for [xcf], [xret] and [xlet]\n\n- do not use quotations in [xret], that is fragile as they will be\n  parsed in an unknown context. This is why [xret] wasn't working in the\n  proof of [print_spec] in basisProgramScript\n\n- properly handle name clashes in [xlet] (just add primes to the\n  introduced name if there's a clash)\n\n- call [reduce_tac] at the end of [xcf], to properly reduce the\n  [if is_bound_Fun .. then .. else] appearing in the let case\n\nThis addresses all the side remarks of #137","distinct":true,"url":"https://api.github.com/repos/CakeML/cakeml/commits/c266d00350134fd39fb83d596f29d574c9a05c12"},{"sha":"2041cb84726c840246da5d4ef18e6bc6d35dd8a7","author":{"name":"Armael","email":"685e678634892b7d707059b1800da7ebe1b90d3d@ens-lyon.fr"},"message":"[xsimpl] now simplifies [IO _ _ ns] if ns is the same on both sides\n\nCloses #137","distinct":true,"url":"https://api.github.com/repos/CakeML/cakeml/commits/2041cb84726c840246da5d4ef18e6bc6d35dd8a7"}]}
{"actor":{"display_login":"Armael"}}