summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ExtractToFStar.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 1d45b239..5d772c04 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -235,7 +235,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
*)
let get_fun_name (name : name) : string =
match name with
- | [ name ] -> name
+ | [ _module; name ] -> name
| _ -> failwith ("Unexpected name shape: " ^ Print.name_to_string name)
in
let fun_name (_fid : A.fun_id) (fname : name) (num_rgs : int)