1 files changed, 0 insertions, 57 deletions
diff --git a/src/ExtractAst.ml b/src/ExtractAst.ml
deleted file mode 100644
index dd793291..00000000
--- a/src/ExtractAst.ml
+++ /dev/null
@@ -1,57 +0,0 @@
-(** This module defines the AST which is to be extracted to generate code.
-    This AST is voluntarily as simple as possible, so that the extraction
-    can focus on pretty-printing and on the syntax specific to the different
-    provers.
-    
-    TODO: we don't use this...
- *)
-
-type constant_value = Pure.constant_value
-
-type pattern =
-  | PatVar of string
-  | PatDummy
-  | PatEnum of string * pattern list
-      (** Enum: the constructor name (tuple if `None`) and the fields.
-          Note that we never use structures as patters: we access the fields one
-          by one.
-       *)
-  | PatTuple of pattern list
-
-(** We want to keep terms a little bit structured, for pretty printing.
-    See the `FieldProj` and the `Record` cases, for instance.
- *)
-type term =
-  | Constant of constant_value
-  | Var of string
-  | FieldProj of term * term
-      (** `x.y`
-
-           Of course, we can always use projectors like `record_get_y x`:
-           this variant is for pretty-printing.
-           
-           Note that `FieldProj` are generated when translating `place` from
-           the "pure" AST.
-       *)
-  | App of term * term
-  | Let of bool * pattern * term * term
-  | If of term * term * term
-  | Switch of term * (pattern * term) list
-  | Ascribed of term * term  (** `x <: ty` *)
-  | Tuple of term list
-  | Record of (string * term) list
-      (** In case a record has named fields, we try to use them, to generate
-          code like: `{ x = 3; y = true; }`
-          Otherwise, we can use `App` (with the record constructor).
-       *)
-
-type fun_decl = {
-  name : string;
-  inputs : pattern list;
-      (** We can match over the inputs, hence the use of [pattern]. In practice,
-          we use [PatVar] and [PatDummy].
-       *)
-  input_tys : term list;
-  output_ty : term;
-  body : term;
-}