diff options
| author | Thomas Bauereiss | 2019-01-17 01:20:33 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-01-17 01:20:33 +0000 |
| commit | 7ebe7fe5a37959b9004548b4287dbfc1f6faa087 (patch) | |
| tree | ebb50f11d57eb1e95a492c7be1b5dd8e51b7e86e /src/pretty_print.mli | |
| parent | 63fa9e0e2807e4b5fc3f825e6914a2fab5de37e3 (diff) | |
Work around an issue with type abbreviations in HOL
If we use the bitlist representation of bitvectors, the type argument in
type abbreviations such as "bits('n)" becomes dead, which confuses HOL;
as a workaround, expand type synonyms in this case.
Diffstat (limited to 'src/pretty_print.mli')
| -rw-r--r-- | src/pretty_print.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 2aaf5318..5537f42c 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -52,4 +52,4 @@ open Ast open Type_check (* Prints on formatter the defs as Lem Ast nodes *) -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit +val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> Env.t -> tannot defs -> string -> unit |