summaryrefslogtreecommitdiff
path: root/extraction/convert
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/convert')
-rwxr-xr-xextraction/convert6
1 files changed, 0 insertions, 6 deletions
diff --git a/extraction/convert b/extraction/convert
deleted file mode 100755
index 94ec38e..0000000
--- a/extraction/convert
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/usr/bin/perl -pi
-
-s/\bList\b/CoqList/g;
-s/\bString\b/CoqString/g;
-s/^open Int$/open CoqInt/;
-