Merge pull request #83 from AeneasVerif/son/backs

Remove the option to split the forward/backward functions

1 files changed, 2 insertions, 13 deletions

diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml
index 88438872..05877b5a 100644
--- a/compiler/TranslateCore.ml
+++ b/compiler/TranslateCore.ml
@@ -8,19 +8,8 @@ let log = Logging.translate_log
 
 type trans_ctx = decls_ctx [@@deriving show]
 type fun_and_loops = { f : Pure.fun_decl; loops : Pure.fun_decl list }
-type pure_fun_translation_no_loops = Pure.fun_decl * Pure.fun_decl list
-
-type pure_fun_translation = {
-  keep_fwd : bool;
-      (** Should we extract the forward function?
-
-          If the forward function returns `()` and there is exactly one
-          backward function, we may merge the forward into the backward
-          function and thus don't extract the forward function)?
-       *)
-  fwd : fun_and_loops;
-  backs : fun_and_loops list;
-}
+type pure_fun_translation_no_loops = Pure.fun_decl
+type pure_fun_translation = fun_and_loops
 
 let trans_ctx_to_fmt_env (ctx : trans_ctx) : Print.fmt_env =
   Print.Contexts.decls_ctx_to_fmt_env ctx