2 files changed, 23 insertions, 3 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8ad87c8e..e5710394 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -183,6 +183,7 @@ let keywords () =
           "unsafe";
           "where";
           "with";
+          "opaque_defs";
         ]
   in
   List.concat [ named_unops; named_binops; misc ]
@@ -738,11 +739,18 @@ let mk_formatter_and_names_map (ctx : trans_ctx) (crate_name : string)
   let names_map = initialize_names_map fmt (names_map_init ()) in
   (fmt, names_map)
 
-(** In Coq, a group of definitions must be ended with a "." *)
+(** In some provers, groups of definitions must be delimited.
+
+    - in Coq, *every* group (including singletons) must end with "."
+    - in Lean, groups of mutually recursive definitions must end with "end"
+ *)
 let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
   if !backend = Coq && decl_is_last_from_group kind then (
     F.pp_print_cut fmt ();
     F.pp_print_string fmt ".")
+  else if !backend = Lean && kind = MutRecLast then (
+    F.pp_print_cut fmt ();
+    F.pp_print_string fmt "end")
 
 let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar -> "unit"
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 781766ee..8250f813 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -686,14 +686,26 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
      definition for OpaqueDefs, which is a structure, in which each field is one
      of the functions marked as Opaque. We emit the `structure ...` bit here,
      then rely on `extract_fun_decl` to be aware of this, and skip the keyword
-     (e.g. "axiom" or "val") so as to generate valid syntax for records. *)
+     (e.g. "axiom" or "val") so as to generate valid syntax for records.
+
+     We also generate such a structure only if there actually are opaque
+     definitions.
+  *)
   let wrap_in_sig =
     config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean
+    &&
+    let _, opaque_funs = module_has_opaque_decls ctx in
+    opaque_funs
   in
   if wrap_in_sig then (
+    (* We change the name of the structure depending on whether we *only*
+       extract opaque definitions, or if we extract all definitions *)
+    let struct_name =
+      if config.extract_transparent then "Definitions" else "OpaqueDefs"
+    in
     Format.pp_print_break fmt 0 0;
     Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr;
-    Format.pp_print_string fmt "structure OpaqueDefs where";
+    Format.pp_print_string fmt ("structure " ^ struct_name ^ " where");
     Format.pp_print_break fmt 0 0);
   List.iter export_decl_group ctx.crate.declarations;