summaryrefslogtreecommitdiff
path: root/src/process_file.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/process_file.mli')
-rw-r--r--src/process_file.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/process_file.mli b/src/process_file.mli
index f91fa064..b15523bb 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -43,6 +43,7 @@
val parse_file : string -> Parse_ast.defs
val convert_ast : Parse_ast.defs -> unit Ast.defs
val check_ast: unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
+val monomorphise_ast : ((string * int) * string) list -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
@@ -53,7 +54,6 @@ val opt_new_typecheck : bool ref
val opt_just_check : bool ref
val opt_ddump_tc_ast : bool ref
val opt_dno_cast : bool ref
-val opt_mono_split : ((string * int) * string) list ref
type out_type =
| Lem_ast_out