diff options
author | Son Ho | 2023-07-06 12:20:28 +0200 |
---|---|---|
committer | Son Ho | 2023-07-06 12:20:28 +0200 |
commit | 7c95800cefc87fad894f8bf855cfc047e713b3a7 (patch) | |
tree | 11b22541914a933bef896b5e765b002ac934faae /compiler/Translate.ml | |
parent | 5ca36bfc50083a01af2b7ae5f75993a520757ef5 (diff) |
Improve the generated comments
Diffstat (limited to '')
-rw-r--r-- | compiler/Translate.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 795674b4..444642c0 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -910,11 +910,14 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : prefixed with the type name to prevent collisions *) match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false in + (* Initialize the names map (we insert the names of the "primitives" + declarations, and insert the names of the local declarations later) *) let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in let fmt, names_map = mk_formatter_and_names_map trans_ctx crate.name variant_concatenate_type_name in + (* Put everything in the context *) let ctx = { ExtractBase.trans_ctx; @@ -923,6 +926,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : indent_incr = 2; use_opaque_pre = !Config.split_files; use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; + fun_name_info = PureUtils.RegularFunIdMap.empty; } in |