summaryrefslogtreecommitdiff
path: root/extraction/fixextract
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/fixextract')
-rwxr-xr-xextraction/fixextract15
1 files changed, 15 insertions, 0 deletions
diff --git a/extraction/fixextract b/extraction/fixextract
new file mode 100755
index 0000000..1ee3c48
--- /dev/null
+++ b/extraction/fixextract
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+echo "Fixing file names..."
+mv list.ml CoqList.ml
+mv list.mli CoqList.mli
+mv string.ml CoqString.ml
+mv string.mli CoqString.mli
+mv int.ml CoqInt.ml
+mv int.mli CoqInt.mli
+
+echo "Conversion List -> CoqList, String -> CoqString, Int -> CoqInt..."
+./convert *.mli *.ml
+
+echo "Patching files..."
+for i in *.patch; do patch < $i; done