diff options
Diffstat (limited to 'src/ExtractToFStar.ml')
| -rw-r--r-- | src/ExtractToFStar.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index e00a4e53..0bcf66bd 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -986,7 +986,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (** Subcase of the app case: ADT field projector. *) and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (original_app : texpression) (proj : proj_kind) + (inside : bool) (original_app : texpression) (proj : projection) (_proj_type_params : ty list) (args : texpression list) : unit = (* We isolate the first argument (if there is), in order to pretty print the * projection (`x.field` instead of `MkAdt?.field x` *) |