diff options
Diffstat (limited to 'lib/extraction/extraction.ml')
-rw-r--r-- | lib/extraction/extraction.ml | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/lib/extraction/extraction.ml b/lib/extraction/extraction.ml new file mode 100644 index 0000000..a737700 --- /dev/null +++ b/lib/extraction/extraction.ml | |||
@@ -0,0 +1,18 @@ | |||
1 | include Prelude | ||
2 | include Interp | ||
3 | include Operational | ||
4 | include Res | ||
5 | |||
6 | (* Stuff that's not part of the paper. Still exposed because we sometimes want | ||
7 | to be able to create a natural number, float, process a list etc. *) | ||
8 | module Internal = struct | ||
9 | module BinNums = BinNums | ||
10 | module Datatypes = Datatypes | ||
11 | module List = List | ||
12 | |||
13 | module Floats = struct | ||
14 | include Floats | ||
15 | include Binary | ||
16 | include SpecFloat | ||
17 | end | ||
18 | end | ||