diff options
| author | Alasdair Armstrong | 2017-07-21 18:30:08 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-21 18:30:08 +0100 |
| commit | a14c066d0c152584cc8799580c2a5fe401f110d0 (patch) | |
| tree | 4d9fbc1ab0e27a5ce65d003e8a133ce65af3d5c0 /src/pretty_print.mli | |
| parent | 79b81722d8cfe3c2c2fa16bbc8643e8243dfa015 (diff) | |
Everything moved to new typechecker
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
Diffstat (limited to 'src/pretty_print.mli')
| -rw-r--r-- | src/pretty_print.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 78764657..24816206 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -41,7 +41,7 @@ (**************************************************************************) open Ast -open Type_check_new +open Type_check (* Prints the defs following source syntax *) val pp_defs : out_channel -> 'a defs -> unit @@ -53,6 +53,3 @@ val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit - - -val pp_format_annot_ascii : Type_internal.tannot -> string |