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 /coq | |
| parent | b6a7b8ee4a5711911b66be6ea4dba3742601b03c (diff) | |
| download | compcert-kvx-d9e1175be2e713232d06c80e9aed33032858e9c7.tar.gz compcert-kvx-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 'coq')
0 files changed, 0 insertions, 0 deletions