diff options
author | Maxime Dénès <maxime.denes@inria.fr> | 2020-09-18 16:52:21 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-18 16:52:21 +0200 |
commit | d9e1175be2e713232d06c80e9aed33032858e9c7 (patch) | |
tree | 0312f4368d6b40660ca2c2d2d30ff45bdc588efc /cparser | |
parent | b6a7b8ee4a5711911b66be6ea4dba3742601b03c (diff) | |
download | compcert-d9e1175be2e713232d06c80e9aed33032858e9c7.tar.gz compcert-d9e1175be2e713232d06c80e9aed33032858e9c7.zip |
Simplify two scripts in Zbits (#369)
Previous scripts were relying on the order in which apply's HO
unification performs reductions, for a goal that could be solved by
reflexivity.
Diffstat (limited to 'cparser')
0 files changed, 0 insertions, 0 deletions