aboutsummaryrefslogtreecommitdiff
path: root/layer/ductusPrinter.mli
diff options
context:
space:
mode:
Diffstat (limited to 'layer/ductusPrinter.mli')
-rwxr-xr-xlayer/ductusPrinter.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/layer/ductusPrinter.mli b/layer/ductusPrinter.mli
deleted file mode 100755
index cdcaa7c..0000000
--- a/layer/ductusPrinter.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-module Make(R:Repr.PRINTER):
- Repr.LAYER with type repr = R.t