summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1ea26d79..7e2efd8a 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -285,9 +285,9 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
| App _ ->
let app, args = destruct_apps e in
extract_App ctx fmt inside app args
- | Abs _ ->
- let xl, e = destruct_abs_list e in
- extract_Abs ctx fmt inside xl e
+ | Lambda _ ->
+ let xl, e = destruct_lambdas e in
+ extract_Lambda ctx fmt inside xl e
| Qualif _ ->
(* We use the app case *)
extract_App ctx fmt inside e []
@@ -574,7 +574,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
(* No argument: shouldn't happen *)
raise (Failure "Unreachable")
-and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+and extract_Lambda (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(xl : typed_pattern list) (e : texpression) : unit =
(* Open a box for the abs expression *)
F.pp_open_hovbox fmt ctx.indent_incr;