Make good progress on the Coq backend

14 files changed, 1058 insertions, 416 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index c9723bd4..95442761 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -1,5 +1,33 @@
 (** Define the global configuration options *)
 
+(** {1 Backend choice} *)
+
+(** The choice of backend *)
+type backend = FStar | Coq
+
+let backend_names = [ "fstar"; "coq" ]
+
+(** Utility to compute the backend from an input parameter *)
+let backend_of_string (b : string) : backend option =
+  match b with "fstar" -> Some FStar | "coq" -> Some Coq | _ -> None
+
+let opt_backend : backend option ref = ref None
+
+let set_backend (b : string) : unit =
+  match backend_of_string b with
+  | Some b -> opt_backend := Some b
+  | None ->
+      (* We shouldn't get there: the string should have been checked as
+         belonging to the proper set *)
+      raise (Failure "Unexpected")
+
+(** The backend to which to extract.
+
+    We initialize it with a default value, but it always gets overwritten:
+    we check that the user provides a backend argument.
+ *)
+let backend = ref FStar
+
 (** {1 Interpreter} *)
 
 (** Check that invariants are maintained whenever we execute a statement *)
@@ -44,6 +72,39 @@ let allow_bottom_below_borrow = true
  *)
 let return_unit_end_abs_with_no_loans = true
 
+(** Forbids using field projectors for structures.
+
+    If we don't use field projectors, whenever we symbolically expand a structure
+    value (note that accessing a structure field in the symbolic execution triggers
+    its expansion), then instead of generating code like this:
+    {[
+       let x1 = s.f1 in
+       let x2 = s.f2 in
+       ...
+    ]}
+
+    we generate code like this:
+    {[
+       let Mkstruct x1 x2 ... = s in
+       ...
+    ]}
+
+    We use this for instance for Coq, because in Coq we can't define groups
+    of mutually recursive records and inductives. In such cases, we extract
+    the structures as inductives, which means that field projectors are not
+    always available.
+
+    TODO: we could define a notation to take care of this.
+    TODO: today dont_use_field_projectors is not useful actually.
+ *)
+let dont_use_field_projectors = ref false
+
+(** Deconstructing ADTs which have only one variant with let-bindings is not always
+    supported: this parameter controls whether we use let-bindings in such situations or not.
+  *)
+
+let always_deconstruct_adts_with_matches = ref false
+
 (** {1 Translation} *)
 
 (** Controls whether we need to use a state to model the external world
@@ -103,7 +164,7 @@ let test_trans_unit_functions = ref false
 
     The body of such clauses must be defined by the user.
  *)
-let extract_decreases_clauses = ref true
+let extract_decreases_clauses = ref false
 
 (** In order to help the user, we can generate "template" decrease clauses
     (i.e., definitions with proper signatures but dummy bodies) in a
@@ -113,10 +174,10 @@ let extract_template_decreases_clauses = ref false
 
 (** {1 Micro passes} *)
 
-(** Some provers like F* don't support the decomposition of return values
+(** Some provers like F* and Coq don't support the decomposition of return values
     in monadic let-bindings:
     {[
-      // NOT supported in F*
+      (* NOT supported in F*/Coq *)
       let (x, y) <-- f ();
       ...
     ]}
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 3059ec2f..5089cb8e 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -33,6 +33,9 @@ let () =
 
   let spec =
     [
+      ( "-backend",
+        Arg.Symbol (backend_names, set_backend),
+        " Specify the backend to which to extract" );
       ("-dest", Arg.Set_string dest_dir, " Specify the output directory");
       ( "-decompose-monads",
         Arg.Set decompose_monadic_let_bindings,
@@ -61,9 +64,9 @@ let () =
         Arg.Set test_trans_unit_functions,
         " Test the translated unit functions with the target theorem\n\
         \                         prover's normalizer" );
-      ( "-no-decreases-clauses",
-        Arg.Clear extract_decreases_clauses,
-        " Do not add decrease clauses to the recursive definitions" );
+      ( "-decreases-clauses",
+        Arg.Set extract_decreases_clauses,
+        " Use decreases clauses for the recursive definitions" );
       ( "-no-state",
         Arg.Clear use_state,
         " Do not use state-error monads, simply use error monads" );
@@ -73,8 +76,8 @@ let () =
       ( "-template-clauses",
         Arg.Set extract_template_decreases_clauses,
         " Generate templates for the required decreases clauses, in a\n\
-        \                         dedicated file. Incompatible with \
-         -no-decreases-clauses" );
+        \                         dedicated file. Reauires -decreases-clauses"
+      );
       ( "-no-split-files",
         Arg.Clear split_files,
         " Don't split the definitions between different files for types,\n\
@@ -98,6 +101,29 @@ let () =
     print_string usage;
     exit 1
   in
+
+  (* Check that the user specified a backend *)
+  let _ =
+    match !opt_backend with
+    | Some b -> backend := b
+    | None ->
+        print_string "Backend not specified (use the `-backend` argument)\n";
+        fail ()
+  in
+
+  (* In the case of Coq, we forbid using field projectors (see the comments for
+     [dont_use_field_projectors]).
+     Also, we always decompose ADT values with matches (decomposing with
+     let-bindings is not supported).
+  *)
+  let _ =
+    match !backend with
+    | FStar -> ()
+    | Coq ->
+        dont_use_field_projectors := true;
+        always_deconstruct_adts_with_matches := true
+  in
+
   (* Retrieve and check the filename *)
   let filename =
     match !filenames with
diff --git a/compiler/ExtractToBackend.ml b/compiler/Extract.ml
index fc04ce90..f9c4d10a 100644
--- a/compiler/ExtractToBackend.ml
+++ b/compiler/Extract.ml
@@ -1,41 +1,19 @@
-(** Extract to F* *)
+(** The generic extraction *)
+(* Turn the whole module into a functor: it is very annoying to carry the
+   the formatter everywhere...
+*)
 
 open Utils
 open Pure
 open PureUtils
 open TranslateCore
-open PureToExtract
+open ExtractBase
 open StringUtils
+open Config
 module F = Format
 
-(** A qualifier for a type definition.
-
-    Controls whether we should use [type ...] or [and ...] (for mutually
-    recursive datatypes).
- *)
-type type_decl_qualif =
-  | Type  (** [type t = ...] *)
-  | And  (** [type t0 = ... and t1 = ...] *)
-  | AssumeType  (** [assume type t] *)
-  | TypeVal  (** In an fsti: [val t : Type0] *)
-
-(** A qualifier for function definitions.
-
-    Controls whether we should use [let ...], [let rec ...] or [and ...],
-    or only generate a declaration with [val] or [assume val]
- *)
-type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
-
-let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string =
-  match qualif with
-  | Let -> "let"
-  | LetRec -> "let rec"
-  | And -> "and"
-  | Val -> "val"
-  | AssumeVal -> "assume val"
-
 (** Small helper to compute the name of an int type *)
-let fstar_int_name (int_ty : integer_type) =
+let int_name (int_ty : integer_type) =
   match int_ty with
   | Isize -> "isize"
   | I8 -> "i8"
@@ -51,17 +29,17 @@ let fstar_int_name (int_ty : integer_type) =
   | U128 -> "u128"
 
 (** Small helper to compute the name of a unary operation *)
-let fstar_unop_name (unop : unop) : string =
+let unop_name (unop : unop) : string =
   match unop with
-  | Not -> "not"
-  | Neg int_ty -> fstar_int_name int_ty ^ "_neg"
+  | Not -> ( match !backend with FStar -> "not" | Coq -> "negb")
+  | Neg int_ty -> int_name int_ty ^ "_neg"
   | Cast _ -> raise (Failure "Unsupported")
 
 (** Small helper to compute the name of a binary operation (note that many
     binary operations like "less than" are extracted to primitive operations,
     like [<].
  *)
-let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
+let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
   let binop =
     match binop with
     | Div -> "div"
@@ -71,64 +49,105 @@ let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | Mul -> "mul"
     | _ -> raise (Failure "Unreachable")
   in
-  fstar_int_name int_ty ^ "_" ^ binop
+  int_name int_ty ^ "_" ^ binop
 
-(** A list of keywords/identifiers used in F* and with which we want to check
-    collision. *)
-let fstar_keywords =
+(** A list of keywords/identifiers used by the backend and with which we
+    want to check collision. *)
+let keywords () =
   let named_unops =
-    fstar_unop_name Not
-    :: List.map (fun it -> fstar_unop_name (Neg it)) T.all_signed_int_types
+    unop_name Not
+    :: List.map (fun it -> unop_name (Neg it)) T.all_signed_int_types
   in
   let named_binops = [ E.Div; Rem; Add; Sub; Mul ] in
   let named_binops =
     List.concat
       (List.map
-         (fun bn ->
-           List.map (fun it -> fstar_named_binop_name bn it) T.all_int_types)
+         (fun bn -> List.map (fun it -> named_binop_name bn it) T.all_int_types)
          named_binops)
   in
   let misc =
-    [
-      "let";
-      "rec";
-      "in";
-      "fn";
-      "val";
-      "int";
-      "nat";
-      "list";
-      "FStar";
-      "FStar.Mul";
-      "type";
-      "match";
-      "with";
-      "assert";
-      "assert_norm";
-      "assume";
-      "Type0";
-      "Type";
-      "unit";
-      "not";
-      "scalar_cast";
-    ]
+    match !backend with
+    | FStar ->
+        [
+          "let";
+          "rec";
+          "in";
+          "fun";
+          "fn";
+          "val";
+          "int";
+          "nat";
+          "list";
+          "FStar";
+          "FStar.Mul";
+          "type";
+          "match";
+          "with";
+          "assert";
+          "assert_norm";
+          "assume";
+          "Type0";
+          "Type";
+          "unit";
+          "not";
+          "scalar_cast";
+        ]
+    | Coq ->
+        [
+          "Record";
+          "Inductive";
+          "Fixpoint";
+          "Definition";
+          "Arguments";
+          "Notation";
+          "Check";
+          "Search";
+          "SearchPattern";
+          "Axiom";
+          "Type";
+          "Set";
+          "let";
+          "rec";
+          "in";
+          "unit";
+          "fun";
+          "type";
+          "int";
+          "nat";
+          "match";
+          "with";
+          "assert";
+          "not";
+          (* [tt] is unit *)
+          "tt";
+          "char_of_byte";
+        ]
   in
   List.concat [ named_unops; named_binops; misc ]
 
-let fstar_assumed_adts : (assumed_ty * string) list =
+let assumed_adts : (assumed_ty * string) list =
   [ (State, "state"); (Result, "result"); (Option, "option"); (Vec, "vec") ]
 
-let fstar_assumed_structs : (assumed_ty * string) list = []
-
-let fstar_assumed_variants : (assumed_ty * VariantId.id * string) list =
-  [
-    (Result, result_return_id, "Return");
-    (Result, result_fail_id, "Fail");
-    (Option, option_some_id, "Some");
-    (Option, option_none_id, "None");
-  ]
-
-let fstar_assumed_llbc_functions :
+let assumed_structs : (assumed_ty * string) list = []
+
+let assumed_variants () : (assumed_ty * VariantId.id * string) list =
+  match !backend with
+  | FStar ->
+      [
+        (Result, result_return_id, "Return");
+        (Result, result_fail_id, "Fail");
+        (Option, option_some_id, "Some");
+        (Option, option_none_id, "None");
+      ]
+  | Coq ->
+      [
+        (Result, result_return_id, "Return");
+        (Result, result_fail_id, "Fail_");
+        (Option, option_some_id, "Some");
+        (Option, option_none_id, "None");
+      ]
+
+let assumed_llbc_functions :
     (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
   let rg0 = Some T.RegionGroupId.zero in
   [
@@ -146,25 +165,27 @@ let fstar_assumed_llbc_functions :
     (VecIndexMut, rg0, "vec_index_mut_back");
   ]
 
-let fstar_assumed_pure_functions : (pure_assumed_fun_id * string) list =
-  [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+let assumed_pure_functions : (pure_assumed_fun_id * string) list =
+  match !backend with
+  | FStar -> [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
+  | Coq -> [ (Return, "return_"); (Fail, "fail_"); (Assert, "massert") ]
 
-let fstar_names_map_init : names_map_init =
+let names_map_init () : names_map_init =
   {
-    keywords = fstar_keywords;
-    assumed_adts = fstar_assumed_adts;
-    assumed_structs = fstar_assumed_structs;
-    assumed_variants = fstar_assumed_variants;
-    assumed_llbc_functions = fstar_assumed_llbc_functions;
-    assumed_pure_functions = fstar_assumed_pure_functions;
+    keywords = keywords ();
+    assumed_adts;
+    assumed_structs;
+    assumed_variants = assumed_variants ();
+    assumed_llbc_functions;
+    assumed_pure_functions;
   }
 
-let fstar_extract_unop (extract_expr : bool -> texpression -> unit)
+let extract_unop (extract_expr : bool -> texpression -> unit)
     (fmt : F.formatter) (inside : bool) (unop : unop) (arg : texpression) : unit
     =
   match unop with
   | Not | Neg _ ->
-      let unop = fstar_unop_name unop in
+      let unop = unop_name unop in
       if inside then F.pp_print_string fmt "(";
       F.pp_print_string fmt unop;
       F.pp_print_space fmt ();
@@ -186,7 +207,7 @@ let fstar_extract_unop (extract_expr : bool -> texpression -> unit)
       extract_expr true arg;
       if inside then F.pp_print_string fmt ")"
 
-let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
+let extract_binop (extract_expr : bool -> texpression -> unit)
     (fmt : F.formatter) (inside : bool) (binop : E.binop)
     (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
   if inside then F.pp_print_string fmt "(";
@@ -203,13 +224,14 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
         | Gt -> ">"
         | _ -> raise (Failure "Unreachable")
       in
+      let binop = match !backend with FStar -> binop | Coq -> "s" ^ binop in
       extract_expr false arg0;
       F.pp_print_space fmt ();
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr false arg1
   | Div | Rem | Add | Sub | Mul ->
-      let binop = fstar_named_binop_name binop int_ty in
+      let binop = named_binop_name binop int_ty in
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr false arg0;
@@ -218,6 +240,52 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
   | BitXor | BitAnd | BitOr | Shl | Shr -> raise Unimplemented);
   if inside then F.pp_print_string fmt ")"
 
+let type_decl_kind_to_qualif (kind : decl_kind)
+    (type_kind : type_decl_kind option) : string =
+  match !backend with
+  | FStar -> (
+      match kind with
+      | SingleNonRec -> "type"
+      | SingleRec -> "type"
+      | MutRecFirst -> "type"
+      | MutRecInner -> "and"
+      | MutRecLast -> "and"
+      | Assumed -> "assume type"
+      | Declared -> "val")
+  | Coq -> (
+      match (kind, type_kind) with
+      | SingleNonRec, Some Enum -> "Inductive"
+      | SingleNonRec, Some Struct -> "Record"
+      | (SingleRec | MutRecFirst), Some _ -> "Inductive"
+      | (MutRecInner | MutRecLast), Some _ ->
+          (* Coq doesn't support groups of mutually recursive definitions which mix
+           * records and inducties: we convert everything to records if this happens
+           *)
+          "with"
+      | (Assumed | Declared), None -> "Axiom"
+      | _ -> raise (Failure "Unexpected"))
+
+let fun_decl_kind_to_qualif (kind : decl_kind) =
+  match !backend with
+  | FStar -> (
+      match kind with
+      | SingleNonRec -> "let"
+      | SingleRec -> "let rec"
+      | MutRecFirst -> "let rec"
+      | MutRecInner -> "and"
+      | MutRecLast -> "and"
+      | Assumed -> "assume val"
+      | Declared -> "val")
+  | Coq -> (
+      match kind with
+      | SingleNonRec -> "Definition"
+      | SingleRec -> "Fixpoint"
+      | MutRecFirst -> "Fixpoint"
+      | MutRecInner -> "with"
+      | MutRecLast -> "with"
+      | Assumed -> "Axiom"
+      | Declared -> "Axiom")
+
 (**
    [ctx]: we use the context to lookup type definitions, to retrieve type names.
    This is used to compute variable names, when they have no basenames: in this
@@ -256,7 +324,7 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
  *)
 let mk_formatter (ctx : trans_ctx) (crate_name : string)
     (variant_concatenate_type_name : bool) : formatter =
-  let int_name = fstar_int_name in
+  let int_name = int_name in
 
   (* Prepare a name.
    * The first id elem is always the crate: if it is the local crate,
@@ -291,7 +359,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   let type_name_to_snake_case name =
     let name = get_type_name name in
     let name = List.map to_snake_case name in
-    String.concat "_" name
+    let name = String.concat "_" name in
+    match !backend with FStar -> name | Coq -> capitalize_first_letter name
   in
   let type_name name = type_name_to_snake_case name ^ "_t" in
   let field_name (def_name : name) (field_id : FieldId.id)
@@ -309,7 +378,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   in
   let struct_constructor (basename : name) : string =
     let tname = type_name basename in
-    "Mk" ^ tname
+    let prefix = match !backend with FStar -> "Mk" | Coq -> "mk" in
+    prefix ^ tname
   in
   let get_fun_name = get_name in
   let fun_name_to_snake_case (fname : fun_name) : string =
@@ -381,7 +451,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
                 assert (List.length cl > 0);
                 let cl = List.map (fun s -> s.[0]) cl in
                 StringUtils.string_of_chars cl)
-        | TypeVar _ -> "x" (* lacking imagination here... *)
+        | TypeVar _ -> (
+            (* TODO: use "t" also for F* *)
+            match !backend with
+            | FStar -> "x" (* lacking inspiration here... *)
+            | Coq -> "t" (* lacking inspiration here... *))
         | Bool -> "b"
         | Char -> "c"
         | Integer _ -> "i"
@@ -390,22 +464,51 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
         | Array _ | Slice _ -> raise Unimplemented)
   in
   let type_var_basename (_varset : StringSet.t) (basename : string) : string =
-    (* This is *not* a no-op: type variables in Rust often start with
-     * a capital letter *)
-    to_snake_case basename
+    (* Rust type variables are snake-case and start with a capital letter *)
+    match !backend with
+    | FStar ->
+        (* This is *not* a no-op: this removes the capital letter *)
+        to_snake_case basename
+    | Coq -> basename
   in
   let append_index (basename : string) (i : int) : string =
     basename ^ string_of_int i
   in
 
-  let extract_primitive_value (fmt : F.formatter) (_inside : bool)
+  let extract_primitive_value (fmt : F.formatter) (inside : bool)
       (cv : primitive_value) : unit =
     match cv with
-    | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+    | Scalar sv -> (
+        match !backend with
+        | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value)
+        | Coq ->
+            if inside then F.pp_print_string fmt "(";
+            (* We need to add parentheses if the value is negative *)
+            if sv.PV.value >= Z.of_int 0 then
+              F.pp_print_string fmt (Z.to_string sv.PV.value)
+            else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty);
+            if inside then F.pp_print_string fmt ")")
     | Bool b ->
         let b = if b then "true" else "false" in
         F.pp_print_string fmt b
-    | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+    | Char c -> (
+        match !backend with
+        | FStar -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+        | Coq ->
+            if inside then F.pp_print_string fmt "(";
+            F.pp_print_string fmt "char_of_byte";
+            F.pp_print_space fmt ();
+            (* Convert the the char to ascii *)
+            let c =
+              let i = Char.code c in
+              let x0 = i / 16 in
+              let x1 = i mod 16 in
+              "Coq.Init.Byte.x" ^ string_of_int x0 ^ string_of_int x1
+            in
+            F.pp_print_string fmt c;
+            if inside then F.pp_print_string fmt ")")
     | String s ->
         (* We need to replace all the line breaks *)
         let s =
@@ -420,6 +523,8 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     char_name = "char";
     int_name;
     str_name = "string";
+    type_decl_kind_to_qualif;
+    fun_decl_kind_to_qualif;
     field_name;
     variant_name;
     struct_constructor;
@@ -431,10 +536,22 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     type_var_basename;
     append_index;
     extract_primitive_value;
-    extract_unop = fstar_extract_unop;
-    extract_binop = fstar_extract_binop;
+    extract_unop;
+    extract_binop;
   }
 
+let mk_formatter_and_names_map (ctx : trans_ctx) (crate_name : string)
+    (variant_concatenate_type_name : bool) : formatter * names_map =
+  let fmt = mk_formatter ctx crate_name variant_concatenate_type_name in
+  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 "." *)
+let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
+  if !backend = Coq && decl_is_last_from_group kind then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt ".")
+
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
  *)
@@ -444,7 +561,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   | Adt (type_id, tys) -> (
       match type_id with
       | Tuple ->
-          (* This is a bit annoying, but in F* [()] is not the unit type:
+          (* This is a bit annoying, but in F*/Coq [()] is not the unit type:
            * we have to write [unit]... *)
           if tys = [] then F.pp_print_string fmt "unit"
           else (
@@ -452,7 +569,8 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
             Collections.List.iter_link
               (fun () ->
                 F.pp_print_space fmt ();
-                F.pp_print_string fmt "&";
+                let product = match !backend with FStar -> "&" | Coq -> "*" in
+                F.pp_print_string fmt product;
                 F.pp_print_space fmt ())
               (extract_ty ctx fmt true) tys;
             F.pp_print_string fmt ")")
@@ -516,68 +634,73 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
   (* Return *)
   ctx
 
-let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_decl) (fields : field list) : unit =
-  (* We want to generate a definition which looks like this:
-     {[
-       type t = { x : int; y : bool; }
-     ]}
-
-     If there isn't enough space on one line:
-     {[
-       type t =
-       {
-         x : int; y : bool;
-       }
-     ]}
-
-     And if there is even less space:
-     {[
-       type t =
-       {
-         x : int;
-         y : bool;
-       }
-     ]}
-
-     Also, in case there are no fields, we need to define the type as [unit]
-     ([type t = {}] doesn't work in F* ).
-  *)
-  (* Note that we already printed: [type t =] *)
-  if fields = [] then (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "unit")
-  else (
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "{";
-    F.pp_print_break fmt 1 ctx.indent_incr;
-    (* The body itself *)
-    F.pp_open_hvbox fmt 0;
-    (* Print the fields *)
-    let print_field (field_id : FieldId.id) (f : field) : unit =
-      let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
-      F.pp_open_box fmt ctx.indent_incr;
-      F.pp_print_string fmt field_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt ":";
-      F.pp_print_space fmt ();
-      extract_ty ctx fmt false f.field_ty;
-      F.pp_print_string fmt ";";
-      F.pp_close_box fmt ()
+(** Print the variants *)
+let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
+    (type_name : string) (type_params : string list) (cons_name : string)
+    (fields : field list) : unit =
+  F.pp_print_space fmt ();
+  F.pp_open_hvbox fmt ctx.indent_incr;
+  (* variant box *)
+  (* [| Cons :]
+   * Note that we really don't want any break above so we print everything
+   * at once. *)
+  F.pp_print_string fmt ("| " ^ cons_name ^ " :");
+  F.pp_print_space fmt ();
+  let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
+      extraction_ctx =
+    (* Open the field box *)
+    F.pp_open_box fmt ctx.indent_incr;
+    (* Print the field names
+     * [  x :]
+     * Note that when printing fields, we register the field names as
+     * *variables*: they don't need to be unique at the top level. *)
+    let ctx =
+      match f.field_name with
+      | None -> ctx
+      | Some field_name ->
+          let var_id = VarId.of_int (FieldId.to_int fid) in
+          let field_name =
+            ctx.fmt.var_basename ctx.names_map.names_set (Some field_name)
+              f.field_ty
+          in
+          let ctx, field_name = ctx_add_var field_name var_id ctx in
+          F.pp_print_string fmt (field_name ^ " :");
+          F.pp_print_space fmt ();
+          ctx
     in
-    let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
-    Collections.List.iter_link (F.pp_print_space fmt)
-      (fun (fid, f) -> print_field fid f)
-      fields;
-    (* Close *)
+    (* Print the field type *)
+    extract_ty ctx fmt false f.field_ty;
+    (* Print the arrow [->]*)
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "->";
+    (* Close the field box *)
     F.pp_close_box fmt ();
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "}")
+    (* Return *)
+    ctx
+  in
+  (* Print the fields *)
+  let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
+  let _ =
+    List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
+  in
+  (* Print the final type *)
+  F.pp_open_hovbox fmt 0;
+  F.pp_print_string fmt type_name;
+  List.iter
+    (fun type_param ->
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt type_param)
+    type_params;
+  F.pp_close_box fmt ();
+  (* Close the variant box *)
+  F.pp_close_box fmt ()
 
+(* TODO: we don' need the [def_name] paramter: it can be retrieved from the context *)
 let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
     (def : type_decl) (def_name : string) (type_params : string list)
     (variants : variant list) : unit =
-  (* We want to generate a definition which looks like this:
+  (* We want to generate a definition which looks like this (taking F* as example):
      {[
        type list a = | Cons : a -> list a -> list a | Nil : list a
      ]}
@@ -609,70 +732,104 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
 
      Note that we already printed: [type s =]
   *)
+  let print_variant variant_id v =
+    let cons_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
+    let fields = v.fields in
+    extract_type_decl_variant ctx fmt def_name type_params cons_name fields
+  in
   (* Print the variants *)
-  let print_variant (variant_id : VariantId.id) (variant : variant) : unit =
-    let variant_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
-    F.pp_print_space fmt ();
-    F.pp_open_hvbox fmt ctx.indent_incr;
-    (* variant box *)
-    (* [| Cons :]
-     * Note that we really don't want any break above so we print everything
-     * at once. *)
-    F.pp_print_string fmt ("| " ^ variant_name ^ " :");
+  let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
+  List.iter (fun (vid, v) -> print_variant vid v) variants
+
+let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
+    (kind : decl_kind) (def : type_decl) (type_params : string list)
+    (fields : field list) : unit =
+  (* We want to generate a definition which looks like this (taking F* as example):
+     {[
+       type t = { x : int; y : bool; }
+     ]}
+
+     If there isn't enough space on one line:
+     {[
+       type t =
+       {
+         x : int; y : bool;
+       }
+     ]}
+
+     And if there is even less space:
+     {[
+       type t =
+       {
+         x : int;
+         y : bool;
+       }
+     ]}
+
+     Also, in case there are no fields, we need to define the type as [unit]
+     ([type t = {}] doesn't work in F* ).
+
+     Coq:
+     ====
+     We need to define the constructor name upon defining the struct (record, in Coq).
+     The syntex is:
+     {[
+       Record Foo = mkFoo { x : int; y : bool; }.
+     }]
+
+     Also, Coq doesn't support groups of mutually recursive inductives and records.
+     This is fine, because we can then define records as inductives, and leverage
+     the fact that when record fields are accessed, the records are symbolically
+     expanded which introduces let bindings of the form: [let RecordCons ... = x in ...].
+     As a consequence, we never use the record projectors (unless we reconstruct
+     them in the micro passes of course).
+  *)
+  (* Note that we already printed: [type t =] *)
+  let is_rec = decl_is_from_rec_group kind in
+  (* If Coq: print the constructor name *)
+  if !backend = Coq && not is_rec then (
     F.pp_print_space fmt ();
-    let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
-        extraction_ctx =
-      (* Open the field box *)
-      F.pp_open_box fmt ctx.indent_incr;
-      (* Print the field names
-       * [  x :]
-       * Note that when printing fields, we register the field names as
-       * *variables*: they don't need to be unique at the top level. *)
-      let ctx =
-        match f.field_name with
-        | None -> ctx
-        | Some field_name ->
-            let var_id = VarId.of_int (FieldId.to_int fid) in
-            let field_name =
-              ctx.fmt.var_basename ctx.names_map.names_set (Some field_name)
-                f.field_ty
-            in
-            let ctx, field_name = ctx_add_var field_name var_id ctx in
-            F.pp_print_string fmt (field_name ^ " :");
-            F.pp_print_space fmt ();
-            ctx
-      in
-      (* Print the field type *)
-      extract_ty ctx fmt false f.field_ty;
-      (* Print the arrow [->]*)
+    F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx));
+  let _ =
+    if !backend = FStar && fields = [] then (
       F.pp_print_space fmt ();
-      F.pp_print_string fmt "->";
-      (* Close the field box *)
-      F.pp_close_box fmt ();
+      F.pp_print_string fmt "unit")
+    else if (not is_rec) || !backend = FStar then (
       F.pp_print_space fmt ();
-      (* Return *)
-      ctx
-    in
-    (* Print the fields *)
-    let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in
-    let _ =
-      List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
-    in
-    (* Print the final type *)
-    F.pp_open_hovbox fmt 0;
-    F.pp_print_string fmt def_name;
-    List.iter
-      (fun type_param ->
+      F.pp_print_string fmt "{";
+      F.pp_print_break fmt 1 ctx.indent_incr;
+      (* The body itself *)
+      F.pp_open_hvbox fmt 0;
+      (* Print the fields *)
+      let print_field (field_id : FieldId.id) (f : field) : unit =
+        let field_name = ctx_get_field (AdtId def.def_id) field_id ctx in
+        F.pp_open_box fmt ctx.indent_incr;
+        F.pp_print_string fmt field_name;
         F.pp_print_space fmt ();
-        F.pp_print_string fmt type_param)
-      type_params;
-    F.pp_close_box fmt ();
-    (* Close the variant box *)
-    F.pp_close_box fmt ()
+        F.pp_print_string fmt ":";
+        F.pp_print_space fmt ();
+        extract_ty ctx fmt false f.field_ty;
+        F.pp_print_string fmt ";";
+        F.pp_close_box fmt ()
+      in
+      let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in
+      Collections.List.iter_link (F.pp_print_space fmt)
+        (fun (fid, f) -> print_field fid f)
+        fields;
+      (* Close *)
+      F.pp_close_box fmt ();
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "}")
+    else (
+      (* We extract for Coq, and we have a recursive record, or a record in
+         a group of mutually recursive types: we extract it as an inductive type
+      *)
+      assert (is_rec && !backend = Coq);
+      let cons_name = ctx_get_struct (AdtId def.def_id) ctx in
+      let def_name = ctx_get_local_type def.def_id ctx in
+      extract_type_decl_variant ctx fmt def_name type_params cons_name fields)
   in
-  (* Print the variants *)
-  let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
-  List.iter (fun (vid, v) -> print_variant vid v) variants
+  ()
 
 (** Extract a type declaration.
 
@@ -680,7 +837,27 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
     registered.
  *)
 let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : type_decl_qualif) (def : type_decl) : unit =
+    (kind : decl_kind) (def : type_decl) : unit =
+  let extract_body =
+    match kind with
+    | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true
+    | Assumed | Declared -> false
+  in
+  let type_kind =
+    if extract_body then
+      match def.kind with
+      | Struct _ -> Some Struct
+      | Enum _ -> Some Enum
+      | Opaque -> None
+    else None
+  in
+  (* If in Coq and the declaration is opaque, it must have the shape:
+     [Axiom Ident : forall (T0 ... Tn : Type), ... -> ... -> ...].
+
+     The boolean [is_opaque_coq] is used to detect this case.
+  *)
+  let is_opaque_coq = !backend = Coq && type_kind = None in
+  let use_forall = is_opaque_coq && def.type_params <> [] in
   (* Retrieve the definition name *)
   let def_name = ctx_get_local_type def.def_id ctx in
   (* Add the type params - note that we need those bindings only for the
@@ -697,16 +874,16 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "type TYPE_NAME" *)
-  let extract_body, qualif =
-    match qualif with
-    | Type -> (true, "type")
-    | And -> (true, "and")
-    | AssumeType -> (false, "assume type")
-    | TypeVal -> (false, "val")
-  in
+  let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   (* Print the type parameters *)
+  let type_keyword = match !backend with FStar -> "Type0" | Coq -> "Type" in
   if def.type_params <> [] then (
+    if use_forall then (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt ":";
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "forall");
     F.pp_print_space fmt ();
     F.pp_print_string fmt "(";
     List.iter
@@ -717,34 +894,117 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
       def.type_params;
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0)");
+    F.pp_print_string fmt (type_keyword ^ ")"));
   (* Print the "=" if we extract the body*)
   if extract_body then (
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "=")
+    let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+    F.pp_print_string fmt eq)
   else (
     (* Otherwise print ": Type0" *)
+    if use_forall then F.pp_print_string fmt ","
+    else (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt ":");
     F.pp_print_space fmt ();
-    F.pp_print_string fmt ":";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0");
+    F.pp_print_string fmt type_keyword);
   (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_close_box fmt ();
   (if extract_body then
    match def.kind with
-   | Struct fields -> extract_type_decl_struct_body ctx_body fmt def fields
+   | Struct fields ->
+       extract_type_decl_struct_body ctx_body fmt kind def type_params fields
    | Enum variants ->
        extract_type_decl_enum_body ctx_body fmt def def_name type_params
          variants
    | Opaque -> raise (Failure "Unreachable"));
+  (* If Coq: end the definition with a "." *)
+  print_decl_end_delimiter fmt kind;
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
+(** Extract extra information for a type (e.g., [Arguments] information in Coq).
+
+    Note that all the names used for extraction should already have been
+    registered.
+ *)
+let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
+    (kind : decl_kind) (decl : type_decl) : unit =
+  match !backend with
+  | FStar -> ()
+  | Coq -> (
+      (* Add the type params - note that we need those bindings only for the
+       * body translation (they are not top-level) *)
+      let _ctx_body, type_params = ctx_add_type_params decl.type_params ctx in
+      (* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *)
+      let extract_arguments_info (cons_name : string) (fields : 'a list) : unit
+          =
+        (* Add a break before *)
+        F.pp_print_break fmt 0 0;
+        (* Open a box *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        (* Small utility *)
+        let print_type_vars () =
+          List.iter
+            (fun (var : string) ->
+              F.pp_print_string fmt ("{" ^ var ^ "}");
+              F.pp_print_space fmt ())
+            type_params
+        in
+        let print_fields () =
+          List.iter
+            (fun _ ->
+              F.pp_print_string fmt "_";
+              F.pp_print_space fmt ())
+            fields
+        in
+        F.pp_print_break fmt 0 0;
+        F.pp_print_string fmt "Arguments";
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt cons_name;
+        F.pp_print_space fmt ();
+        print_type_vars ();
+        print_fields ();
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt ".";
+
+        (* Close the box *)
+        F.pp_close_box fmt ()
+      in
+
+      (* Generate the [Arguments] instruction *)
+      match decl.kind with
+      | Opaque -> ()
+      | Struct fields ->
+          let adt_id = AdtId decl.def_id in
+          (* Generate the instruction for the record constructor *)
+          let cons_name = ctx_get_struct adt_id ctx in
+          extract_arguments_info cons_name fields;
+          (* Generate the instruction for the record projectors, if there are *)
+          let is_rec = decl_is_from_rec_group kind in
+          if not is_rec then
+            FieldId.iteri
+              (fun fid _ ->
+                let cons_name = ctx_get_field adt_id fid ctx in
+                extract_arguments_info cons_name [])
+              fields;
+          (* Add breaks to insert new lines between definitions *)
+          F.pp_print_break fmt 0 0
+      | Enum variants ->
+          (* Generate the instructions *)
+          VariantId.iteri
+            (fun vid (v : variant) ->
+              let cons_name = ctx_get_variant (AdtId decl.def_id) vid ctx in
+              extract_arguments_info cons_name v.fields)
+            variants;
+          (* Add breaks to insert new lines between definitions *)
+          F.pp_print_break fmt 0 0)
+
 (** Extract the state type declaration. *)
 let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
-    (qualif : type_decl_qualif) : unit =
+    (kind : decl_kind) : unit =
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment  *)
@@ -755,27 +1015,48 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
   F.pp_open_hvbox fmt 0;
   (* Retrieve the name *)
   let state_name = ctx_get_assumed_type State ctx in
-  (* The qualif should be [AssumeType] or [TypeVal] *)
-  (match qualif with
-  | Type | And -> raise (Failure "Unexpected")
-  | AssumeType ->
-      F.pp_print_string fmt "assume";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "type";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt state_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt ":";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "Type0"
-  | TypeVal ->
-      F.pp_print_string fmt "val";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt state_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt ":";
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "Type0");
+  (* The kind should be [Assumed] or [Declared] *)
+  (match kind with
+  | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast ->
+      raise (Failure "Unexpected")
+  | Assumed -> (
+      match !backend with
+      | FStar ->
+          F.pp_print_string fmt "assume";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "type";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt state_name;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "Type0"
+      | Coq ->
+          F.pp_print_string fmt "Axiom";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt state_name;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "Type.")
+  | Declared -> (
+      match !backend with
+      | FStar ->
+          F.pp_print_string fmt "val";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt state_name;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "Type0"
+      | Coq ->
+          F.pp_print_string fmt "Axiom";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt state_name;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "Type."));
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
@@ -813,7 +1094,8 @@ let extract_global_decl_register_names (ctx : extraction_ctx)
     Note that patterns can introduce new variables: we thus return an extraction
     context updated with new bindings.
     
-    TODO: we don't need something very generic anymore
+    TODO: we don't need something very generic anymore (some definitions used
+    to be polymorphic).
  *)
 let extract_adt_g_value
     (extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
@@ -823,17 +1105,23 @@ let extract_adt_g_value
   match ty with
   | Adt (Tuple, _) ->
       (* Tuple *)
-      F.pp_print_string fmt "(";
-      let ctx =
-        Collections.List.fold_left_link
-          (fun () ->
-            F.pp_print_string fmt ",";
-            F.pp_print_space fmt ())
-          (fun ctx v -> extract_value ctx false v)
-          ctx field_values
-      in
-      F.pp_print_string fmt ")";
-      ctx
+      (* This is very annoying: in Coq, we can't write [()] for the value of
+         type [unit], we have to write [tt]. *)
+      if !backend = Coq && field_values = [] then (
+        F.pp_print_string fmt "tt";
+        ctx)
+      else (
+        F.pp_print_string fmt "(";
+        let ctx =
+          Collections.List.fold_left_link
+            (fun () ->
+              F.pp_print_string fmt ",";
+              F.pp_print_space fmt ())
+            (fun ctx v -> extract_value ctx false v)
+            ctx field_values
+        in
+        F.pp_print_string fmt ")";
+        ctx)
   | Adt (adt_id, _) ->
       (* "Regular" ADT *)
       (* We print something of the form: [Cons field0 ... fieldn].
@@ -1014,15 +1302,19 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   | Tuple ->
       (* Tuple *)
       (* For now, we only support fully applied tuple constructors *)
+      (* This is very annoying: in Coq, we can't write [()] for the value of
+         type [unit], we have to write [tt]. *)
       assert (List.length type_args = List.length args);
-      F.pp_print_string fmt "(";
-      Collections.List.iter_link
-        (fun () ->
-          F.pp_print_string fmt ",";
-          F.pp_print_space fmt ())
-        (fun v -> extract_texpression ctx fmt false v)
-        args;
-      F.pp_print_string fmt ")"
+      if !backend = Coq && args = [] then F.pp_print_string fmt "tt"
+      else (
+        F.pp_print_string fmt "(";
+        Collections.List.iter_link
+          (fun () ->
+            F.pp_print_string fmt ",";
+            F.pp_print_space fmt ())
+          (fun v -> extract_texpression ctx fmt false v)
+          args;
+        F.pp_print_string fmt ")")
   | _ ->
       (* "Regular" ADT *)
       (* We print something of the form: [Cons field0 ... fieldn].
@@ -1062,7 +1354,10 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
       (* We allow to break where the "." appears *)
       F.pp_print_break fmt 0 0;
       F.pp_print_string fmt ".";
-      F.pp_print_string fmt field_name;
+      (* If in Coq, the field projection has to be parenthesized *)
+      (match !backend with
+      | FStar -> F.pp_print_string fmt field_name
+      | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
       (* Close the box *)
       F.pp_close_box fmt ()
   | arg :: args ->
@@ -1114,7 +1409,8 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
        * a variable *)
       let ctx = extract_typed_pattern ctx fmt true lv in
       F.pp_print_space fmt ();
-      F.pp_print_string fmt "<--";
+      let arrow = match !backend with FStar -> "<--" | Coq -> "<-" in
+      F.pp_print_string fmt arrow;
       F.pp_print_space fmt ();
       extract_texpression ctx fmt false re;
       F.pp_print_string fmt ";";
@@ -1124,7 +1420,8 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       F.pp_print_space fmt ();
       let ctx = extract_typed_pattern ctx fmt true lv in
       F.pp_print_space fmt ();
-      F.pp_print_string fmt "=";
+      let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+      F.pp_print_string fmt eq;
       F.pp_print_space fmt ();
       extract_texpression ctx fmt false re;
       F.pp_print_space fmt ();
@@ -1170,15 +1467,18 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_open_hovbox fmt ctx.indent_incr;
         (* Print the [begin] if necessary *)
         let parenth = PureUtils.let_group_requires_parentheses e_branch in
+        let left_delim, right_delim =
+          match !backend with FStar -> ("begin", "end") | Coq -> ("(", ")")
+        in
         if parenth then (
-          F.pp_print_string fmt "begin";
+          F.pp_print_string fmt left_delim;
           F.pp_print_space fmt ());
         (* Print the branch expression *)
         extract_texpression ctx fmt false e_branch;
         (* Close the [begin ... end ] *)
         if parenth then (
           F.pp_print_space fmt ();
-          F.pp_print_string fmt "end");
+          F.pp_print_string fmt right_delim);
         (* Close the box for the branch *)
         F.pp_close_box fmt ();
         (* Close the box for the then/else+branch *)
@@ -1191,7 +1491,10 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       (* Open a box for the [match ... with] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* Print the [match ... with] *)
-      F.pp_print_string fmt "begin match";
+      let match_begin =
+        match !backend with FStar -> "begin match" | Coq -> "match"
+      in
+      F.pp_print_string fmt match_begin;
       F.pp_print_space fmt ();
       let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
@@ -1210,7 +1513,8 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_space fmt ();
         let ctx = extract_typed_pattern ctx fmt false br.pat in
         F.pp_print_space fmt ();
-        F.pp_print_string fmt "->";
+        let arrow = match !backend with FStar -> "->" | Coq -> "=>" in
+        F.pp_print_string fmt arrow;
         F.pp_print_space fmt ();
         (* Open a box for the branch *)
         F.pp_open_hovbox fmt ctx.indent_incr;
@@ -1258,7 +1562,8 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
       def.signature.type_params;
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "Type0)";
+    let type_keyword = match !backend with FStar -> "Type0" | Coq -> "Type" in
+    F.pp_print_string fmt (type_keyword ^ ")");
     (* Close the box for the type parameters *)
     F.pp_close_box fmt ();
     F.pp_print_space fmt ());
@@ -1305,8 +1610,10 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
 
 (** Extract a decrease clause function template body.
 
+    Only for F*.
+
     In order to help the user, we can generate a template for the functions
-    required by the decreases clauses. We simply generate definitions of
+    required by the decreases clauses for. We simply generate definitions of
     the following form in a separate file:
     {[
       let f_decrease (t : Type0) (x : t) : nat = admit()
@@ -1319,6 +1626,7 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
  *)
 let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_decl) : unit =
+  assert (!backend = FStar);
   (* Retrieve the function name *)
   let def_name = ctx_get_decreases_clause def.def_id ctx in
   (* Add a break before *)
@@ -1371,14 +1679,10 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     it is useful for the decrease clause.
  *)
 let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
-    unit =
+    (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
   assert (not def.is_global_decl_body);
   (* Retrieve the function name *)
   let def_name = ctx_get_local_function def.def_id def.back_id ctx in
-  (* (* Add the type parameters - note that we need those bindings only for the
-     * body translation (they are not top-level) *)
-      let ctx, _ = ctx_add_type_params def.signature.type_params ctx in *)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
@@ -1392,9 +1696,21 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
   let is_opaque = Option.is_none def.body in
-  let qualif = fun_decl_qualif_keyword qualif in
+  (* If in Coq and the declaration is opaque, it must have the shape:
+     [Axiom Ident : forall (T0 ... Tn : Type), ... -> ... -> ...].
+
+     The boolean [is_opaque_coq] is used to detect this case.
+  *)
+  let is_opaque_coq = !backend = Coq && is_opaque in
+  let use_forall = is_opaque_coq && def.signature.type_params <> [] in
+  (* *)
+  let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
   F.pp_print_string fmt (qualif ^ " " ^ def_name);
   F.pp_print_space fmt ();
+  if use_forall then (
+    F.pp_print_string fmt ":";
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "forall");
   (* Open a box for "(PARAMS) : EFFECT =" *)
   F.pp_open_hvbox fmt 0;
   (* Open a box for "(PARAMS)" *)
@@ -1408,7 +1724,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
    * the bindings we introduced above.
    * TODO: figure out a cleaner way *)
   let _ =
-    F.pp_print_string fmt ":";
+    if use_forall then F.pp_print_string fmt "," else F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
     (* Open a box for the EFFECT *)
     F.pp_open_hvbox fmt 0;
@@ -1421,6 +1737,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     if is_opaque then extract_fun_input_parameters_types ctx fmt def;
     (* [Tot] *)
     if has_decreases_clause then (
+      assert (!backend = FStar);
       F.pp_print_string fmt "Tot";
       F.pp_print_space fmt ());
     extract_ty ctx fmt has_decreases_clause def.signature.output;
@@ -1429,6 +1746,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (* Print the decrease clause - rk.: a function with a decreases clause
      * is necessarily a transparent function *)
     if has_decreases_clause then (
+      assert (!backend = FStar);
       F.pp_print_space fmt ();
       (* Open a box for the decrease clause *)
       F.pp_open_hovbox fmt 0;
@@ -1476,7 +1794,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the "=" *)
   if not is_opaque then (
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "=");
+    let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+    F.pp_print_string fmt eq);
   (* Close the box for "(PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
   (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *)
@@ -1487,16 +1806,22 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_open_hvbox fmt 0;
     (* Extract the body *)
     let _ = extract_texpression ctx_body fmt false (Option.get def.body).body in
+    (* Coq: add a "." *)
+    print_decl_end_delimiter fmt kind;
     (* Close the box for the body *)
     F.pp_close_box fmt ());
+  (* Coq: add a "." *)
+  if is_opaque_coq then print_decl_end_delimiter fmt kind;
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
-(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY" with a custom body extractor *)
+(** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY"
+    with a custom body extractor
+ *)
 let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (qualif : fun_decl_qualif) (name : string) (ty : ty)
+    (kind : decl_kind) (name : string) (ty : ty)
     (extract_body : (F.formatter -> unit) Option.t) : unit =
   let is_opaque = Option.is_none extract_body in
 
@@ -1506,7 +1831,9 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Print "QUALIF NAME " *)
-  F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name);
+  F.pp_print_string fmt (ctx.fmt.fun_decl_kind_to_qualif kind);
+  F.pp_print_space fmt ();
+  F.pp_print_string fmt name;
   F.pp_print_space fmt ();
 
   (* Open ": TYPE =" box (depth=2) *)
@@ -1525,7 +1852,8 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   if not is_opaque then (
     (* Print " =" *)
     F.pp_print_space fmt ();
-    F.pp_print_string fmt "=");
+    let eq = match !backend with FStar -> "=" | Coq -> ":=" in
+    F.pp_print_string fmt eq);
   (* Close ": TYPE =" box (depth=2) *)
   F.pp_close_box fmt ();
   (* Close "QUALIF NAME : TYPE =" box (depth=1) *)
@@ -1539,16 +1867,22 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
     (Option.get extract_body) fmt;
     (* Close "BODY" box (depth=1) *)
     F.pp_close_box fmt ());
+
+  (* Coq: add a "." *)
+  print_decl_end_delimiter fmt Declared;
+
   (* Close the definition box (depth=0) *)
   F.pp_close_box fmt ()
 
 (** Extract a global declaration.
-    We generate the body which computes the global value separately from the value declaration itself.
+
+    We generate the body which computes the global value separately from the
+    value declaration itself.
 
     For example in Rust,
     [static X: u32 = 3;]
 
-    will be translated to:
+    will be translated to the following F*:
     [let x_body : result u32 = Return 3]
     [let x_c : u32 = eval_global x_body]
  *)
@@ -1578,22 +1912,37 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   in
   match body.body with
   | None ->
-      let qualif = if interface then Val else AssumeVal in
-      extract_global_decl_body ctx fmt qualif decl_name decl_ty None
+      let kind = if interface then Declared else Assumed in
+      extract_global_decl_body ctx fmt kind decl_name decl_ty None
   | Some body ->
-      extract_global_decl_body ctx fmt Let body_name body_ty
+      extract_global_decl_body ctx fmt SingleNonRec body_name body_ty
         (Some (fun fmt -> extract_texpression ctx fmt false body.body));
       F.pp_print_break fmt 0 0;
-      extract_global_decl_body ctx fmt Let decl_name decl_ty
-        (Some (fun fmt -> F.pp_print_string fmt ("eval_global " ^ body_name)));
+      extract_global_decl_body ctx fmt SingleNonRec decl_name decl_ty
+        (Some
+           (fun fmt ->
+             let body =
+               match !backend with
+               | FStar -> "eval_global " ^ body_name
+               | Coq -> body_name ^ "%global"
+             in
+             F.pp_print_string fmt body));
+      (* Add a break to insert lines between declarations *)
       F.pp_print_break fmt 0 0
 
 (** Extract a unit test, if the function is a unit function (takes no
     parameters, returns unit).
     
-    A unit test simply checks that the function normalizes to [Return ()]:
+    A unit test simply checks that the function normalizes to [Return ()].
+
+    F*:
     {[
-      let _ = assert_norm (FUNCTION () = Return ())
+      let _ = assert_norm (FUNCTION = Return ())
+    ]}
+
+    Coq:
+    {[
+      Check (FUNCTION)%return).
     ]}
  *)
 let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
@@ -1616,21 +1965,34 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     (* Open a box for the test *)
     F.pp_open_hovbox fmt ctx.indent_incr;
     (* Print the test *)
-    F.pp_print_string fmt "let _ =";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "assert_norm";
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "(";
-    let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
-    F.pp_print_string fmt fun_name;
-    if sg.inputs <> [] then (
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "()");
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "=";
-    F.pp_print_space fmt ();
-    let success = ctx_get_variant (Assumed Result) result_return_id ctx in
-    F.pp_print_string fmt (success ^ " ())");
+    (match !backend with
+    | FStar ->
+        F.pp_print_string fmt "let _ =";
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "assert_norm";
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "(";
+        let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
+        F.pp_print_string fmt fun_name;
+        if sg.inputs <> [] then (
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "()");
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "=";
+        F.pp_print_space fmt ();
+        let success = ctx_get_variant (Assumed Result) result_return_id ctx in
+        F.pp_print_string fmt (success ^ " ())")
+    | Coq ->
+        F.pp_print_string fmt "Check";
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "(";
+        let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
+        F.pp_print_string fmt fun_name;
+        if sg.inputs <> [] then (
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "()");
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt ")%return.");
     (* Close the box for the test *)
     F.pp_close_box fmt ();
     (* Add a break after *)
diff --git a/compiler/PureToExtract.ml b/compiler/ExtractBase.ml
index 25ad6713..33939e6a 100644
--- a/compiler/PureToExtract.ml
+++ b/compiler/ExtractBase.ml
@@ -1,8 +1,4 @@
-(** This module is used to extract the pure ASTs to various theorem provers.
-    It defines utilities and helpers to make the work as easy as possible:
-    we try to factorize as much as possible the different extractions to the
-    backends we target.
- *)
+(** Define base utilities for the extraction *)
 
 open Pure
 open TranslateCore
@@ -33,8 +29,79 @@ type type_name = Names.type_name
 type global_name = Names.global_name
 type fun_name = Names.fun_name
 
+(** Characterizes a declaration.
+
+    Is in particular useful to derive the proper keywords to introduce the
+    declarations/definitions.
+ *)
+type decl_kind =
+  | SingleNonRec
+      (** A single, non-recursive definition.
+
+          F*:  [let x = ...]
+          Coq: [Definition x := ...]
+       *)
+  | SingleRec
+      (** A single, recursive definition.
+
+          F*:  [let rec x = ...]
+          Coq: [Fixpoint x := ...]
+       *)
+  | MutRecFirst
+      (** The first definition of a group of mutually-recursive definitions.
+
+          F*:  [type x0 = ... and x1 = ...]
+          Coq: [Fixpoing x0 := ... with x1 := ...]
+       *)
+  | MutRecInner
+      (** An inner definition in a group of mutually-recursive definitions. *)
+  | MutRecLast
+      (** The last definition in a group of mutually-recursive definitions.
+
+          We need this because in some theorem provers like Coq, we need to
+          delimit group of mutually recursive definitions (in particular, we
+          need to insert an end delimiter).
+       *)
+  | Assumed
+      (** An assumed definition.
+
+         F*:  [assume val x]
+         Coq: [Axiom x : Type.]
+      *)
+  | Declared
+      (** Declare a type in an interface or a module signature.
+
+          Rem.: for now, in Coq, we don't declare module signatures: we
+          thus assume the corresponding declarations.
+
+          F*:  [val x : Type0]
+          Coq: [Axiom x : Type.]
+       *)
+
+(** Return [true] if the declaration is the last from its group of declarations.
+
+    We need this because in some provers (e.g., Coq), we need to delimit the
+    end of a (group of) definition(s) (in Coq: with a ".").
+ *)
+let decl_is_last_from_group (kind : decl_kind) : bool =
+  match kind with
+  | SingleNonRec | SingleRec | MutRecLast | Assumed | Declared -> true
+  | MutRecFirst | MutRecInner -> false
+
+let decl_is_from_rec_group (kind : decl_kind) : bool =
+  match kind with
+  | SingleNonRec | Assumed | Declared -> false
+  | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true
+
+let decl_is_from_mut_rec_group (kind : decl_kind) : bool =
+  match kind with
+  | SingleNonRec | SingleRec | Assumed | Declared -> false
+  | MutRecFirst | MutRecInner | MutRecLast -> true
+
 (* TODO: this should a module we give to a functor! *)
 
+type type_decl_kind = Enum | Struct
+
 (** A formatter's role is twofold:
     1. Come up with name suggestions.
     For instance, provided some information about a function (its basename,
@@ -51,6 +118,16 @@ type formatter = {
   char_name : string;
   int_name : integer_type -> string;
   str_name : string;
+  type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string;
+      (** Compute the qualified for a type definition/declaration.
+    
+          For instance: "type", "and", etc.
+       *)
+  fun_decl_kind_to_qualif : decl_kind -> string;
+      (** Compute the qualified for a function definition/declaration.
+    
+          For instance: "let", "let rec", "and", etc.
+       *)
   field_name : name -> FieldId.id -> string option -> string;
       (** Inputs:
           - type name
diff --git a/compiler/ExtractToCoq.ml b/compiler/ExtractToCoq.ml
new file mode 100644
index 00000000..3681adc3
--- /dev/null
+++ b/compiler/ExtractToCoq.ml
@@ -0,0 +1,8 @@
+(** Utilities for the extraction to Coq *)
+
+open Utils
+open Pure
+open TranslateCore
+open ExtractBase
+open StringUtils
+module F = Format
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
new file mode 100644
index 00000000..21a6fc8f
--- /dev/null
+++ b/compiler/ExtractToFStar.ml
@@ -0,0 +1,8 @@
+(** Utilities for the extraction to F* *)
+
+open Utils
+open Pure
+open TranslateCore
+open ExtractBase
+open StringUtils
+module F = Format
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 5f22506b..1d57fa5b 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -18,8 +18,8 @@ let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
 (** Logger for PureMicroPasses *)
 let pure_micro_passes_log = L.get_logger "MainLogger.PureMicroPasses"
 
-(** Logger for PureToExtract *)
-let pure_to_extract_log = L.get_logger "MainLogger.PureToExtract"
+(** Logger for ExtractBase *)
+let pure_to_extract_log = L.get_logger "MainLogger.ExtractBase"
 
 (** Logger for Interpreter *)
 let interpreter_log = L.get_logger "MainLogger.Interpreter"
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 30fc4989..7b261516 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1250,6 +1250,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl option =
         (lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Simplify the aggregated ADTs.
+
          Ex.:
          {[
            type struct = { f0 : nat; f1 : nat }
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index ff55f322..5a024d9e 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -398,9 +398,9 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
       let cons = { e = Qualif qualif; ty } in
       mk_apps cons vl
 
-let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id)
+let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id option)
     (vl : typed_pattern list) : typed_pattern =
-  let value = PatAdt { variant_id = Some variant_id; field_values = vl } in
+  let value = PatAdt { variant_id; field_values = vl } in
   { value; ty = adt_ty }
 
 let ty_as_integer (t : ty) : T.integer_type =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 235e33e4..9d95db7f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -26,6 +26,7 @@ type mplace = {
   projection : E.projection;
       (** We store the projection because we can, but it is actually not that useful *)
 }
+[@@deriving show]
 
 type call_id =
   | Fun of A.fun_id * V.FunCallId.id
@@ -43,6 +44,7 @@ type call = {
   dest : V.symbolic_value;
   dest_place : mplace option;  (** Meta information *)
 }
+[@@deriving show]
 
 (** Meta information, not necessary for synthesis but useful to guide it to
     generate a pretty output.
@@ -51,6 +53,7 @@ type call = {
 type meta =
   | Assignment of mplace * V.typed_value * mplace option
       (** We generated an assignment (destination, assigned value, src) *)
+[@@deriving show]
 
 (** **Rk.:** here, {!expression} is not at all equivalent to the expressions
     used in LLBC: they are a first step towards lambda-calculus expressions.
@@ -108,3 +111,4 @@ and expansion =
       T.integer_type * (V.scalar_value * expression) list * expression
       (** An integer expansion (i.e, a switch over an integer). The last
           expression is for the "otherwise" branch. *)
+[@@deriving show]
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index a327c785..62be5efd 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1578,8 +1578,17 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       (* We don't do the same thing if there is a branching or not *)
       match branches with
       | [] -> raise (Failure "Unreachable")
-      | [ (variant_id, svl, branch) ] -> (
-          (* There is exactly one branch: no branching *)
+      | [ (variant_id, svl, branch) ]
+        when not
+               (TypesUtils.ty_is_custom_adt sv.V.sv_ty
+               && !Config.always_deconstruct_adts_with_matches) -> (
+          (* There is exactly one branch: no branching.
+
+             We can decompose the ADT value with a let-binding, unless
+             the backend doesn't support this (see {!Config.always_deconstruct_adts_with_matches}):
+             we *ignore* this branch (and go to the next one) if the ADT is a custom
+             adt, and [always_deconstruct_adts_with_matches] is true.
+          *)
           let type_id, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
           let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
           let branch = translate_expression branch ctx in
@@ -1588,9 +1597,16 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
               (* Detect if this is an enumeration or not *)
               let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
               let is_enum = type_decl_is_enum tdef in
-              if is_enum then
-                (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
-                let variant_id = Option.get variant_id in
+              (* We deconstruct the ADT with a let-binding in two situations:
+                 - if the ADT is an enumeration (which must have exactly one branch)
+                 - if we forbid using field projectors.
+
+                   We forbid using field projectors in some situations, for example
+                   if the backend is Coq. See  '!Config.dont_use_field_projectors}.
+              *)
+              let use_let = is_enum || !Config.dont_use_field_projectors in
+              if use_let then
+                (* Introduce a let binding which expands the ADT *)
                 let lvars =
                   List.map (fun v -> mk_typed_pattern_from_var v None) vars
                 in
@@ -1665,8 +1681,6 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
           let translate_branch (variant_id : T.VariantId.id option)
               (svl : V.symbolic_value list) (branch : S.expression) :
               match_branch =
-            (* There *must* be a variant id - otherwise there can't be several branches *)
-            let variant_id = Option.get variant_id in
             let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
             let vars =
               List.map (fun x -> mk_typed_pattern_from_var x None) vars
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 79d1c913..b2a28710 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -293,7 +293,7 @@ let translate_module_to_pure (crate : A.crate) :
 (** Extraction context *)
 type gen_ctx = {
   crate : A.crate;
-  extract_ctx : PureToExtract.extraction_ctx;
+  extract_ctx : ExtractBase.extraction_ctx;
   trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
   trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
   functions_with_decreases_clause : A.FunDeclId.Set.t;
@@ -342,30 +342,41 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
  *)
 let extract_definitions (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) : unit =
-  (* Export the definition groups to the file, in the proper order *)
-  let export_type (qualif : ExtractToBackend.type_decl_qualif)
-      (id : Pure.TypeDeclId.id) : unit =
-    (* Retrive the declaration *)
+  (* Export the definition groups to the file, in the proper order.
+     - [extract_decl]: extract the type declaration (if not filtered)
+     - [extract_extra_info]: extra the extra type information (e.g.,
+       the [Arguments] information in Coq).
+  *)
+  let export_type (kind : ExtractBase.decl_kind) (id : Pure.TypeDeclId.id)
+      (extract_decl : bool) (extract_extra_info : bool) : unit =
+    (* Retrieve the declaration *)
     let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
-    (* Update the qualifier, if the type is opaque *)
-    let is_opaque, qualif =
+    (* Update the kind, if the type is opaque *)
+    let is_opaque, kind =
       match def.kind with
-      | Enum _ | Struct _ -> (false, qualif)
+      | Enum _ | Struct _ -> (false, kind)
       | Opaque ->
-          let qualif =
-            if config.interface then ExtractToBackend.TypeVal
-            else ExtractToBackend.AssumeType
+          let kind =
+            if config.interface then ExtractBase.Declared
+            else ExtractBase.Assumed
           in
-          (true, qualif)
+          (true, kind)
     in
     (* Extract, if the config instructs to do so (depending on whether the type
      * is opaque or not) *)
     if
       (is_opaque && config.extract_opaque)
       || ((not is_opaque) && config.extract_transparent)
-    then ExtractToBackend.extract_type_decl ctx.extract_ctx fmt qualif def
+    then (
+      if extract_decl then
+        Extract.extract_type_decl ctx.extract_ctx fmt kind def;
+      if extract_extra_info then
+        Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def)
   in
 
+  let export_type_decl kind id = export_type kind id true false in
+  let export_type_extra_info kind id = export_type kind id false true in
+
   (* Utility to check a function has a decrease clause *)
   let has_decreases_clause (def : Pure.fun_decl) : bool =
     A.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
@@ -393,8 +404,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
         (fun (_, (fwd, _)) ->
           let has_decr_clause = has_decreases_clause fwd in
           if has_decr_clause then
-            ExtractToBackend.extract_template_decreases_clause ctx.extract_ctx fmt
-              fwd)
+            Extract.extract_template_decreases_clause ctx.extract_ctx fmt fwd)
         pure_ls;
     (* Extract the function definitions *)
     (if config.extract_fun_decls then
@@ -408,17 +418,25 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
          else true
        else false
      in
+     let fls_length = List.length fls in
      List.iteri
        (fun i (fwd_def, def) ->
          let is_opaque = Option.is_none fwd_def.Pure.body in
-         let qualif =
+         let kind =
            if is_opaque then
-             if config.interface then ExtractToBackend.Val
-             else ExtractToBackend.AssumeVal
-           else if not is_rec then ExtractToBackend.Let
+             if config.interface then ExtractBase.Declared
+             else ExtractBase.Assumed
+           else if not is_rec then ExtractBase.SingleNonRec
            else if is_mut_rec then
-             if i = 0 then ExtractToBackend.LetRec else ExtractToBackend.And
-           else ExtractToBackend.LetRec
+             (* If the functions are mutually recursive, we need to distinguish:
+              * - the first of the group
+              * - the last of the group
+              * - the inner functions
+              *)
+             if i = 0 then ExtractBase.MutRecFirst
+             else if i = fls_length - 1 then ExtractBase.MutRecLast
+             else ExtractBase.MutRecInner
+           else ExtractBase.SingleRec
          in
          let has_decr_clause =
            has_decreases_clause def && config.extract_decreases_clauses
@@ -428,15 +446,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            ((not is_opaque) && config.extract_transparent)
            || (is_opaque && config.extract_opaque)
          then
-           ExtractToBackend.extract_fun_decl ctx.extract_ctx fmt qualif
-             has_decr_clause def)
+           Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause def)
        fls);
     (* Insert unit tests if necessary *)
     if config.test_trans_unit_functions then
       List.iter
         (fun (keep_fwd, (fwd, _)) ->
           if keep_fwd then
-            ExtractToBackend.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
+            Extract.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
         pure_ls
   in
 
@@ -454,32 +471,49 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
       ((not is_opaque) && config.extract_transparent)
       || (is_opaque && config.extract_opaque)
     then
-      ExtractToBackend.extract_global_decl ctx.extract_ctx fmt global body
+      Extract.extract_global_decl ctx.extract_ctx fmt global body
         config.interface
   in
 
   let export_state_type () : unit =
-    let qualif =
-      if config.interface then ExtractToBackend.TypeVal
-      else ExtractToBackend.AssumeType
+    let kind =
+      if config.interface then ExtractBase.Declared else ExtractBase.Assumed
     in
-    ExtractToBackend.extract_state_type fmt ctx.extract_ctx qualif
+    Extract.extract_state_type fmt ctx.extract_ctx kind
   in
 
   let export_decl (decl : A.declaration_group) : unit =
     match decl with
     | Type (NonRec id) ->
-        if config.extract_types then export_type ExtractToBackend.Type id
+        if config.extract_types then (
+          let kind = ExtractBase.SingleNonRec in
+          (* Export the type declaration *)
+          export_type_decl kind id;
+          (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
+          export_type_extra_info kind id)
     | Type (Rec ids) ->
         (* Rk.: we shouldn't have (mutually) recursive opaque types *)
-        if config.extract_types then
+        let num_decls = List.length ids in
+        let is_mut_rec = num_decls > 1 in
+        if config.extract_types then (
+          let kind_from_index i =
+            if not is_mut_rec then ExtractBase.SingleRec
+            else if i = 0 then ExtractBase.MutRecFirst
+            else if i = num_decls - 1 then ExtractBase.MutRecLast
+            else ExtractBase.MutRecInner
+          in
+          (* Extract the type declarations *)
+          List.iteri
+            (fun i id ->
+              let kind = kind_from_index i in
+              export_type_decl kind id)
+            ids;
+          (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
           List.iteri
             (fun i id ->
-              let qualif =
-                if i = 0 then ExtractToBackend.Type else ExtractToBackend.And
-              in
-              export_type qualif id)
-            ids
+              let kind = kind_from_index i in
+              export_type_extra_info kind id)
+            ids)
     | Fun (NonRec id) ->
         (* Lookup *)
         let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
@@ -527,15 +561,33 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   (* Create the header *)
   Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
   Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg;
-  Printf.fprintf out "module %s\n" module_name;
-  Printf.fprintf out "open Primitives\n";
-  (* Add the custom imports *)
-  List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
-  (* Add the custom includes *)
-  List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
-  (* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
-  Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n";
-
+  (match !Config.backend with
+  | FStar ->
+      Printf.fprintf out "module %s\n" module_name;
+      Printf.fprintf out "open Primitives\n";
+      (* Add the custom imports *)
+      List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
+      (* Add the custom includes *)
+      List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
+      (* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
+      Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n"
+  | Coq ->
+      Printf.fprintf out "Require Import Primitives.\n";
+      Printf.fprintf out "Import Primitives.\n";
+      Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n";
+      Printf.fprintf out "Local Open Scope Primitives_scope.\n";
+
+      (* Add the custom imports *)
+      List.iter
+        (fun m -> Printf.fprintf out "Require Import %s .\n" m)
+        custom_imports;
+      (* Add the custom includes *)
+      List.iter
+        (fun m ->
+          Printf.fprintf out "Require Export %s .\n" m;
+          Printf.fprintf out "Import %s .\n" m)
+        custom_includes;
+      Printf.fprintf out "Module %s .\n" module_name);
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
   Format.pp_set_margin fmt 80;
@@ -550,6 +602,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   Format.pp_close_box fmt ();
   Format.pp_print_newline fmt ();
 
+  (* Close the module *)
+  (match !Config.backend with
+  | FStar -> ()
+  | Coq -> Printf.fprintf out "End %s .\n" module_name);
+
   (* Some logging *)
   log#linfo (lazy ("Generated: " ^ filename));
 
@@ -568,17 +625,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
    * We initialize the names map by registering the keywords used in the
    * language, as well as some primitive names ("u32", etc.) *)
   let variant_concatenate_type_name = true in
-  let fstar_fmt =
-    ExtractToBackend.mk_formatter trans_ctx crate.name
+  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
-  let names_map =
-    PureToExtract.initialize_names_map fstar_fmt
-      ExtractToBackend.fstar_names_map_init
-  in
-  let ctx =
-    { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
-  in
+  let ctx = { ExtractBase.trans_ctx; names_map; fmt; indent_incr = 2 } in
 
   (* We need to compute which functions are recursive, in order to know
    * whether we should generate a decrease clause or not. *)
@@ -596,7 +648,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
    * sure there are no name clashes. *)
   let ctx =
     List.fold_left
-      (fun ctx def -> ExtractToBackend.extract_type_decl_register_names ctx def)
+      (fun ctx def -> Extract.extract_type_decl_register_names ctx def)
       ctx trans_types
   in
 
@@ -612,14 +664,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
         let is_global = (fst def).Pure.is_global_decl_body in
         if is_global then ctx
         else
-          ExtractToBackend.extract_fun_decl_register_names ctx keep_fwd
-            gen_decr_clause def)
+          Extract.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause
+            def)
       ctx trans_funs
   in
 
   let ctx =
-    List.fold_left ExtractToBackend.extract_global_decl_register_names ctx
-      crate.globals
+    List.fold_left Extract.extract_global_decl_register_names ctx crate.globals
   in
 
   (* Open the output file *)
@@ -658,12 +709,17 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     (* Create a directory with *default* permissions *)
     Core_unix.mkdir_p dest_dir);
 
-  (* Copy "Primitives.fst" *)
+  (* Copy the "Primitives" file *)
   let _ =
     (* Retrieve the executable's directory *)
     let exe_dir = Filename.dirname Sys.argv.(0) in
-    let src = open_in (exe_dir ^ "/backends/fstar/Primitives.fst") in
-    let tgt_filename = Filename.concat dest_dir "Primitives.fst" in
+    let primitives_src, primitives_destname =
+      match !Config.backend with
+      | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst")
+      | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v")
+    in
+    let src = open_in (exe_dir ^ primitives_src) in
+    let tgt_filename = Filename.concat dest_dir primitives_destname in
     let tgt = open_out tgt_filename in
     (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
     try
@@ -689,6 +745,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     }
   in
 
+  let module_delimiter =
+    match !Config.backend with FStar -> "." | Coq -> "__"
+  in
+
   (* Extract one or several files, depending on the configuration *)
   if !Config.split_files then (
     let base_gen_config =
@@ -712,9 +772,16 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
 
     (* Extract the types *)
     (* If there are opaque types, we extract in an interface *)
-    let types_filename_ext = if has_opaque_types then ".fsti" else ".fst" in
-    let types_filename = extract_filebasename ^ ".Types" ^ types_filename_ext in
-    let types_module = module_name ^ ".Types" in
+    let types_filename_ext =
+      match !Config.backend with
+      | FStar -> if has_opaque_types then ".fsti" else ".fst"
+      | Coq -> if has_opaque_types then ".v" else ".v"
+    in
+    let types_file_suffix = module_delimiter ^ "Types" in
+    let types_filename =
+      extract_filebasename ^ types_file_suffix ^ types_filename_ext
+    in
+    let types_module = module_name ^ types_file_suffix in
     let types_config =
       {
         base_gen_config with
@@ -733,8 +800,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       && not (A.FunDeclId.Set.is_empty rec_functions)
     in
     (if needs_clauses_module && !Config.extract_template_decreases_clauses then
-     let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
-     let clauses_module = module_name ^ ".Clauses.Template" in
+     let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in
+     let clauses_file_suffix =
+       module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"
+     in
+     let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in
+     let clauses_module = module_name ^ clauses_file_suffix in
      let clauses_config =
        { base_gen_config with extract_template_decreases_clauses = true }
      in
@@ -745,8 +816,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     (* Extract the opaque functions, if needed *)
     let opaque_funs_module =
       if has_opaque_funs then (
-        let opaque_filename = extract_filebasename ^ ".Opaque.fsti" in
-        let opaque_module = module_name ^ ".Opaque" in
+        let ext = match !Config.backend with FStar -> ".fsti" | Coq -> ".v" in
+        let opaque_file_suffix = module_delimiter ^ "Opaque" in
+        let opaque_filename = extract_filebasename ^ opaque_file_suffix ^ ext in
+        let opaque_module = module_name ^ opaque_file_suffix in
         let opaque_config =
           {
             base_gen_config with
@@ -763,8 +836,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
     in
 
     (* Extract the functions *)
-    let fun_filename = extract_filebasename ^ ".Funs.fst" in
-    let fun_module = module_name ^ ".Funs" in
+    let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in
+    let fun_file_suffix = module_delimiter ^ "Funs" in
+    let fun_filename = extract_filebasename ^ fun_file_suffix ^ ext in
+    let fun_module = module_name ^ fun_file_suffix in
     let fun_config =
       {
         base_gen_config with
@@ -773,7 +848,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       }
     in
     let clauses_module =
-      if needs_clauses_module then [ module_name ^ ".Clauses" ] else []
+      if needs_clauses_module then
+        [ module_name ^ module_delimiter ^ "Clauses" ]
+      else []
     in
     extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
       ": function definitions" []
@@ -794,6 +871,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
       }
     in
     (* Add the extension for F* *)
-    let extract_filename = extract_filebasename ^ ".fst" in
+    let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in
+    let extract_filename = extract_filebasename ^ ext in
     extract_file gen_config gen_ctx extract_filename crate.A.name module_name ""
       [] []
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 44b22f9f..046f0482 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -817,3 +817,4 @@ type symbolic_expansion =
   | SeAdt of (VariantId.id option * symbolic_value list)
   | SeMutRef of BorrowId.id * symbolic_value
   | SeSharedRef of BorrowId.Set.t * symbolic_value
+[@@deriving show]
diff --git a/compiler/dune b/compiler/dune
index 10aa9b10..b530340b 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -20,7 +20,10 @@
   Cps
   Expressions
   ExpressionsUtils
-  ExtractToBackend
+  Extract
+  ExtractBase
+  ExtractToCoq
+  ExtractToFStar
   FunsAnalysis
   Identifiers
   InterpreterBorrowsCore
@@ -44,7 +47,6 @@
   PrintPure
   PureMicroPasses
   Pure
-  PureToExtract
   PureTypeCheck
   PureUtils
   Scalars