diff --git a/test-suite/cram/dune b/test-suite/cram/dune deleted file mode 100644 index f322ba0a7fc5..000000000000 --- a/test-suite/cram/dune +++ /dev/null @@ -1,2 +0,0 @@ -(cram - (deps %{bin:coqc} %{project_root}/theories/extraction/Extraction.vo %{project_root}/theories/Arith/PeanoNat.vo)) diff --git a/test-suite/cram/extraction-output1.t/a.v b/test-suite/cram/extraction-output1.t/a.v deleted file mode 100644 index 1375f2575f14..000000000000 --- a/test-suite/cram/extraction-output1.t/a.v +++ /dev/null @@ -1,4 +0,0 @@ -From Coq Require Import Extraction. -Extraction "bar" nat. -Set Extraction Output Directory "foo". -Extraction "zar" nat. diff --git a/test-suite/cram/extraction-output1.t/run.t b/test-suite/cram/extraction-output1.t/run.t deleted file mode 100644 index 1794e108b26a..000000000000 --- a/test-suite/cram/extraction-output1.t/run.t +++ /dev/null @@ -1,27 +0,0 @@ -Testing the output directory of extraction - $ ls - a.v - - $ coqc a.v - File "./a.v", line 2, characters 0-21: - Warning: Setting extraction output directory by default to - "$TESTCASE_ROOT". - Use "Set Extraction Output Directory" to set a different directory for - extracted files to appear in. [extraction-default-directory,extraction] -Extraction is able to create ouput directories as specified by the user - - $ ls . foo - .: - a.glob - a.v - a.vo - a.vok - a.vos - bar.ml - bar.mli - foo - - foo: - zar.ml - zar.mli - diff --git a/test-suite/cram/extraction-output2.t/a.v b/test-suite/cram/extraction-output2.t/a.v deleted file mode 100644 index 1375f2575f14..000000000000 --- a/test-suite/cram/extraction-output2.t/a.v +++ /dev/null @@ -1,4 +0,0 @@ -From Coq Require Import Extraction. -Extraction "bar" nat. -Set Extraction Output Directory "foo". -Extraction "zar" nat. diff --git a/test-suite/cram/extraction-output2.t/run.t b/test-suite/cram/extraction-output2.t/run.t deleted file mode 100644 index 682816985e56..000000000000 --- a/test-suite/cram/extraction-output2.t/run.t +++ /dev/null @@ -1,50 +0,0 @@ -Testing the output directory of extraction - - $ cat > b.v << EOF - > From Coq Require PeanoNat. - > Recursive Extraction Library PeanoNat. - > EOF - - $ coqc b.v -require-import Extraction -set "Extraction Output Directory"="bar" - File "./b.v", line 2, characters 0-38: - Warning: The extraction is currently set to bypass opacity, the following - opaque constant bodies have been accessed - : PeanoNat.Nat.OddT_2 PeanoNat.Nat.OddT_1 PeanoNat.Nat.odd_OddT - PeanoNat.Nat.EvenT_OddT_rect PeanoNat.Nat.EvenT_S_OddT - PeanoNat.Nat.OddT_S_EvenT PeanoNat.Nat.Even_EvenT - PeanoNat.Nat.EvenT_OddT_dec PeanoNat.Nat.even_EvenT - PeanoNat.Nat.OddT_EvenT_rect PeanoNat.Nat.Odd_OddT PeanoNat.Nat.EvenT_2 - PeanoNat.Nat.EvenT_0. - [extraction-opaque-accessed,extraction] - - $ ls . bar - .: - a.v - b.glob - b.v - b.vo - b.vok - b.vos - bar - - bar: - Bool.ml - Bool.mli - Datatypes.ml - Datatypes.mli - DecidableClass.ml - DecidableClass.mli - Decimal.ml - Decimal.mli - Hexadecimal.ml - Hexadecimal.mli - Logic.ml - Logic.mli - Number.ml - Number.mli - PeanoNat.ml - PeanoNat.mli - Specif.ml - Specif.mli - Wf.ml - Wf.mli