aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/float_syntax.ml
diff options
context:
space:
mode:
authorPierre Roux2020-04-02 15:42:59 +0200
committerPierre Roux2020-05-09 18:02:00 +0200
commit2d6c26cfab4055ff2b25a311544bdf59363686a7 (patch)
treed1a13ab723641b06a6e455418d6e570a854a3865 /plugins/syntax/float_syntax.ml
parentda4a78d9fe25b000005a968d17c2e17bb42b71f4 (diff)
Hexadecimal: conversion to/from Coq strings
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions