diff options
Diffstat (limited to 'extraction/convert')
-rwxr-xr-x | extraction/convert | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/extraction/convert b/extraction/convert deleted file mode 100755 index 94ec38e8..00000000 --- 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/; - |