aboutsummaryrefslogtreecommitdiffstats
path: root/lib/extraction/extraction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/extraction/extraction.ml')
-rw-r--r--lib/extraction/extraction.ml18
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 @@
1include Prelude
2include Interp
3include Operational
4include 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. *)
8module 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
18end