diff options
author | Vincent Laporte <vbgl@users.noreply.github.com> | 2018-09-14 12:15:01 +0000 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-09-14 14:15:01 +0200 |
commit | fad5113b1216ce735565c44b3bb2a21b76d692aa (patch) | |
tree | 90d44e1cb8a153eba1ea2592613163ed159be6b0 /runtime/x86_32/i64_smod.S | |
parent | 932d40637eaa84e6d335a0a997eacc35379e2bec (diff) | |
download | compcert-fad5113b1216ce735565c44b3bb2a21b76d692aa.tar.gz compcert-fad5113b1216ce735565c44b3bb2a21b76d692aa.zip |
flocq: minor cleaning (#257)
This change avoids relying on generated names, making the proof script compatible with ongoing evolutions of the `zify` tactic.
A similar cleanup was already performed in Flocq's master sources.
Diffstat (limited to 'runtime/x86_32/i64_smod.S')
0 files changed, 0 insertions, 0 deletions