summaryrefslogtreecommitdiff
path: root/src/ExtractToFStar.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/ExtractToFStar.ml')
-rw-r--r--src/ExtractToFStar.ml7
1 files changed, 3 insertions, 4 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 19e17260..e00a4e53 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -872,12 +872,11 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Top-level qualifier *)
match qualif.id with
| Func fun_id ->
- extract_function_call ctx fmt inside fun_id qualif.type_params args
+ extract_function_call ctx fmt inside fun_id qualif.type_args args
| AdtCons adt_cons_id ->
- extract_adt_cons ctx fmt inside adt_cons_id qualif.type_params args
+ extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
| Proj proj ->
- extract_field_projector ctx fmt inside app proj qualif.type_params
- args)
+ extract_field_projector ctx fmt inside app proj qualif.type_args args)
| _ ->
(* "Regular" expression *)
(* Open parentheses *)