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/process_file.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/process_file.mli')
| -rw-r--r-- | src/process_file.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/process_file.mli b/src/process_file.mli index 1d4d629a..181443fb 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -78,7 +78,7 @@ type out_type = val output : string -> (* The path to the library *) out_type -> (* Backend kind *) - (string * Type_check.tannot Ast.defs) list -> (*File names paired with definitions *) + (string * Type_check.Env.t * Type_check.tannot Ast.defs) list -> (*File names paired with definitions *) unit (** [always_replace_files] determines whether Sail only updates modified files. |