diff options
Diffstat (limited to 'extraction')
-rwxr-xr-x | extraction/convert | 6 | ||||
-rw-r--r-- | extraction/extraction.v | 3 | ||||
-rwxr-xr-x | extraction/fixextract | 11 |
3 files changed, 3 insertions, 17 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/; - diff --git a/extraction/extraction.v b/extraction/extraction.v index d74e192e..137ddb06 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -82,6 +82,9 @@ Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y". Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y". +(* Avoid name clashes *) +Extraction Blacklist List String Int. + (* Go! *) Cd "extraction". Recursive Extraction Library Compiler. diff --git a/extraction/fixextract b/extraction/fixextract index 1ee3c484..86ebdbdd 100755 --- a/extraction/fixextract +++ b/extraction/fixextract @@ -1,15 +1,4 @@ #!/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 |