aboutsummaryrefslogtreecommitdiff
path: root/kernel/float64.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-28 21:41:25 +0000
committerGitHub2020-11-28 21:41:25 +0000
commit9992bb15d4f90fc0cf3aa2854beb209bc5effac6 (patch)
tree6664a13c0bde2b0d00a22f815532fc4b1646ea9b /kernel/float64.mli
parent7514bc25c6e8dffeb58ae9af0916dac83953d337 (diff)
parenta1daae8800194166662c87e11a974a6ae3d24a4d (diff)
Merge PR #13502: A small fix for freshness in the `change` tactic
Reviewed-by: herbelin
Diffstat (limited to 'kernel/float64.mli')
0 files changed, 0 insertions, 0 deletions