summaryrefslogtreecommitdiff
path: root/src/lib/sounds/repr.mli
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2021-09-03 17:44:44 +0200
committerSébastien Dailly <sebastien@chimrod.com>2021-09-03 17:44:44 +0200
commit66cb521749672586fd5b1182b14e3c5d44829616 (patch)
tree92adafc00225ce4775c3a98c59ac56582d4b0b5a /src/lib/sounds/repr.mli
parent025faa27075a15d9f3b2cb7f29c2228d3e4cb049 (diff)
Extract representation in dedicated library
Diffstat (limited to 'src/lib/sounds/repr.mli')
-rw-r--r--src/lib/sounds/repr.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/lib/sounds/repr.mli b/src/lib/sounds/repr.mli
deleted file mode 100644
index 7e2e035..0000000
--- a/src/lib/sounds/repr.mli
+++ /dev/null
@@ -1 +0,0 @@
-include Sig.REPR with type t = String.t