Commits

Thomas Tuerk committed fd388de

cleanup representation of targets

The type of typed-ast targets was represented as "Target.target option". None represented the identity target, which is
not representable explicitly in the untyped ast. This commit renames "Target.target" to
"Target.non_ident_target" and introduces a new variant type "Target.target" to replace the option-type.
Moreover, the use of "Target.target" is cleaned-up in many places.

  • Participants
  • Parent commits aa250da

Comments (0)

Files changed (31)

   val lex_skip : Ast.lex_skip -> Ulib.Text.t
   val need_space : Output.t' -> Output.t' -> bool
 
-  val target : Target.target option
+  val target : Target.target
 
   val path_sep : t
   val list_sep : t
     let (d2,s2) = f y in
       not d1 && not d2 && s1 = s2
 
-  let target = None
+  let target = Target_ident
 
   let path_sep = kwd "."
   let list_sep = kwd ";"
 
 module Html : Target = struct
   include Identity 
-  let target = Some Target_html
+  let target = Target_no_ident Target_html
 
   let forall = kwd "∀"
   let exists = kwd "∃"
 
   let need_space x y = false
 
-  let target = Some Target_tex
+  let target = Target_no_ident Target_tex
 
   let tkwd s = kwd (String.concat "" ["\\lemkw{"; s;  "}"])
   let tkwdl s = kwd (String.concat "" ["\\lemkw{"; s;  "}"]) ^ texspace
 module Ocaml : Target = struct
   include Identity 
 
-  let target = Some Target_ocaml
+  let target = Target_no_ident Target_ocaml
 
   let path_sep = kwd "."
 
     | Ast.Ws(r) -> r
     | Ast.Nl -> r"\n"
 
-  let target = Some Target_isa
+  let target = Target_no_ident Target_isa
 
   (* TODO : write need_space *)
 
     let (d2,s2) = f y in
       not d1 && not d2 && s1 = s2
 
-  let target = Some Target_hol
+  let target = Target_no_ident Target_hol
 
   let path_sep = meta "$"
   let list_sep = kwd ";"
 
 module B = Backend_common.Make (struct
   let env = A.env
-  let target_opt = T.target
+  let target = T.target
   let id_format_args =  (T.infix_op_format, T.path_sep)    
 end);;
 
   let avoid = A.avoid
 end);;
 
-let is_identity_target = match T.target with
-    None -> true
-  | Some Target_isa   -> false
-  | Some Target_hol   -> false
-  | Some Target_coq   -> false
-  | Some Target_ocaml -> false
-  | Some Target_html  -> true
-  | Some Target_tex   -> true
-
 let rec interspace os = 
   match os with
   | [] -> [emp]
         ws s3 ^
         T.recup_end
   | Field(e,s,fd) ->
-      if (T.target = Some Target_isa) then
+      if (T.target = Target_no_ident Target_isa) then
         kwd "(" ^ T.field_access_start ^ 
         field_ident_to_output fd ^
         T.field_access_end ^ 
       T.set_start ^
       exp e1 ^
       ws s2 ^
-      (if T.target = Some Target_isa then 
+      (if T.target = Target_no_ident Target_isa then 
          (if (is_var_tup_exp e1 && NameSet.equal vars (nfmap_domain (C.exp_to_free e1))) then kwd "." else 
           T.setcomp_sep ^
           flat (List.map (fun x -> id Term_var (Name.to_rope x)) (NameSet.elements vars)) ^
 
   (* TODO: Add an Isabelle transformation to nested Quants *)
   | Quant(q,qbs,s2,e) ->
-      if (T.target = Some Target_isa) then 
+      if (T.target = Target_no_ident Target_isa) then 
         block is_user_exp 0 (
         kwd "(" ^ 
         flat (List.map (isa_quant q) qbs) ^
   end ^
   ws s1 ^
   T.def_binding ^
-  exp (if is_identity_target then e else mk_opt_paren_exp e) ^
+  exp (if is_human_target T.target then e else mk_opt_paren_exp e) ^
   T.funcase_end
 
 and funcl tvs (({term = n}, c, ps, topt, s1, e):funcl_aux) =
           | None -> emp 
           | Some(s,t) -> ws s ^ T.typ_sep ^ typ t
       end ^
-      ws s2 ^ T.def_binding ^ exp (if is_identity_target then e else mk_opt_paren_exp e)
+      ws s2 ^ T.def_binding ^ exp (if is_human_target T.target then e else mk_opt_paren_exp e)
   | Let_fun (n, ps, topt, s1, e) ->
       funcl_aux tvs (n.term, ps, topt, s1, e)
 
       end
   | Type_def(s, defs) ->
       let defs = 
-        if T.target = Some Target_hol then 
+        if T.target = Target_no_ident Target_hol then 
           Seplist.map (hol_strip_args (collect_type_names defs)) defs 
         else 
           defs 
       if in_target targets then
         ws s1 ^
         T.def_start ^
-        (if T.target = None then
+        (if T.target = Target_ident then
            targets_opt targets 
          else
            emp) ^
             | (n,n_ref, _, _, _, _)::_ -> Name.strip_lskip (B.const_ref_to_name n.term n_ref)
         in
           T.rec_def_header is_rec is_real_rec s1 s2 n ^
-          (if T.target = None then
+          (if T.target = Target_ident then
              targets_opt targets 
            else
              emp) ^
           else
         emp
   | Val_def(Let_inline(s1,s2,targets,n,c,args,s4,body),tnvs,class_constraints) ->
-      if (T.target = None) then
+      if (T.target = Target_ident) then
         ws s1 ^
         kwd "let" ^
         ws s2 ^
       else
         emp
   | Lemma (sk0, lty, targets, n_opt, sk1, e, sk2) -> 
-      if (not is_identity_target) then emp else
+      if (not (is_human_target T.target)) then emp else
       begin
       let lem_st = match lty with
                      | Ast.Lemma_theorem sk -> "theorem"
       ws sk1 ^ kwd "(" ^ exp e ^ ws sk2 ^ kwd ")")
     end
   | Ident_rename(s1,targets,p,i,s2,(n_new, _)) ->
-      if (T.target = None) then
+      if (T.target = Target_ident) then
         ws s1 ^
         kwd "rename" ^
         targets_opt targets ^
       if in_target targets then
         ws s ^
         T.reln_start ^
-        (if T.target = None then
+        (if T.target = Target_ident then
            targets_opt targets 
          else
            emp) ^
     (fun ((d,s),l) y -> 
        begin
          match T.target with 
-         | Some Target_isa  -> isa_def d (is_trans_loc l)
-         | Some Target_tex  -> raise (Failure "should be unreachable")
-         | Some Target_html -> html_link_def d ^ def d (is_trans_loc l)
+         | Target_no_ident Target_isa  -> isa_def d (is_trans_loc l)
+         | Target_no_ident Target_tex  -> raise (Failure "should be unreachable")
+         | Target_no_ident Target_html -> html_link_def d ^ def d (is_trans_loc l)
          | _ -> def d (is_trans_loc l)
        end ^
 
       let is_simple = true in
       if in_target targets then 
         ws s1 ^ kwd (if is_simple then "definition" else "fun") ^ 
-        (if T.target = None then
+        (if T.target = Target_ident then
            targets_opt targets 
          else
            emp) ^
       if in_target targets then 
         let s2 = Util.option_default None s2_opt in
         ws s1 ^ kwd (if is_rec then "function (sequential)" else "fun") ^ ws s2 ^
-        (if T.target = None then
+        (if T.target = Target_ident then
            targets_opt targets 
          else
            emp) ^
       if in_target targets then
         ws s ^
         T.reln_start ^
-        (if T.target = None then
+        (if T.target = Target_ident then
            targets_opt targets 
          else
            emp) ^
       (fun ((d,s),l) y -> 
          begin
            match T.target with 
-           | Some Target_isa   -> isa_def_extra gf d l 
-           | Some Target_hol   -> hol_def_extra gf d l 
-           | Some Target_ocaml -> ocaml_def_extra gf d l 
+           | Target_no_ident Target_isa   -> isa_def_extra gf d l 
+           | Target_no_ident Target_hol   -> hol_def_extra gf d l 
+           | Target_no_ident Target_ocaml -> ocaml_def_extra gf d l 
            | _ -> emp
          end ^
 
 
 let defs_to_rope ((ds:def list),end_lex_skips) =
   match T.target with
-  | Some Target_tex -> 
+  | Target_no_ident Target_tex -> 
       Ulib.Text.concat (r"") (List.map (function ((d,s),l) -> to_rope_tex_def d) ds) ^^^^
       (match to_rope_option_tex T.lex_skip T.need_space true (ws end_lex_skips) with None -> r"" | Some rr -> 
         r"\\lemdef{\n" ^^^^
 (* for -inc.tex file *)
 let defs_inc ((ds:def list),end_lex_skips) =
   match T.target with
-  | Some Target_tex -> 
+  | Target_no_ident Target_tex -> 
       batrope_pair_concat (List.map (function ((d,s),l) -> batrope_pair_concat (def_tex_inc d)) ds)
   | _ ->
       raise (Failure "defs_inc called on non-tex target")
        (fun ((d,s),l) y ->
           begin match T.target with
 
-              Some Target_isa -> 
+              Target_no_ident Target_isa -> 
                 begin 
                   match d with 
                       Open(s,m) -> 

src/backend_common.ml

         let (subst, x, y) = build_subst params args in
           (Nfmap.insert subst (Name.strip_lskip p.term, Sub(a)), x, y)
 
-let inline_exp l target_opt env was_infix params body tsubst (args : exp list) =
+let inline_exp l (target : Target.non_ident_target) env was_infix params body tsubst (args : exp list) =
   let module C = Exps_in_context(struct let env_opt = Some env;; let avoid = None end) in
   let loc = Ast.Trans("inline_exp", Some l) in
   let (vsubst, leftover_params, leftover_args) = build_subst params args in
   let b = C.exp_subst (tsubst,vsubst) body in
   let stays_infix = match C.exp_to_term b with
-    | Constant id -> Precedence.is_infix (Precedence.get_prec target_opt env id.descr)
+    | Constant id -> Precedence.is_infix (Precedence.get_prec (Target.Target_no_ident target) env id.descr)
     | _ -> false
   in
   if params = [] && was_infix && stays_infix then
          None b None)
 
 
-let inline_exp_macro target_opt env e =
+let inline_exp_macro (target : Target.non_ident_target) env e =
   let l_unk = Ast.Trans("do_substitutions", Some (exp_to_locn e)) in
   let module C = Exps_in_context(struct let env_opt = Some env;; let avoid = None end) in
   let (f,args,was_infix) = strip_app_infix_exp e in
       | Constant(c_id) ->
           let cd = c_env_lookup l_unk env.c_env c_id.descr in
           begin            
-            match Target.Targetmap.apply_opt cd.target_rep target_opt with
+            match Target.Targetmap.apply cd.target_rep target with
               | Some(CR_inline (_, params,body)) ->
                   let tsubst = Types.TNfmap.from_list2 cd.const_tparams c_id.instantiation in
 
                   (* adapt whitespace before body *)
                   let b = (fst (alter_init_lskips (fun _ -> (ident_get_first_lskip c_id, None)) body)) in
-                  Some (inline_exp l_unk target_opt env was_infix params b tsubst args)
+                  Some (inline_exp l_unk target env was_infix params b tsubst args)
               | _ -> None
           end
       | _ -> None
 
 module Make(A : sig 
   val env : env;; 
-  val target_opt : Target.target option;;
+  val target : Target.target;;
   val id_format_args : (Output.id_annot -> Ulib.Text.t -> Output.t) * Output.t
  end) = struct
 
 let const_id_to_ident c_id =
   let l = Ast.Trans ("const_id_to_ident", None) in
   let c_descr = c_env_lookup l A.env.c_env c_id.descr in
-  let i = match Target.Targetmap.apply_opt c_descr.target_rep A.target_opt with
+  let i = match Target.Targetmap.apply_target c_descr.target_rep A.target with
      | None -> resolve_ident_path c_id c_descr.const_binding
      | Some (CR_new_ident (_, _, i)) -> i
      | Some (CR_rename (_, _, n)) -> Ident.rename (resolve_ident_path c_id c_descr.const_binding) n
 
 let constant_application_to_output_simple is_infix_pos arg_f args c_id = begin
   let i = const_id_to_ident c_id in 
-  let const_is_infix = Precedence.is_infix (Precedence.get_prec A.target_opt A.env c_id.descr) in
+  let const_is_infix = Precedence.is_infix (Precedence.get_prec A.target A.env c_id.descr) in
   let is_infix = (is_infix_pos && const_is_infix && (Ident.has_empty_path_prefix i)) in
   let use_infix_notation = ((not is_infix) && const_is_infix) in
   let name = ident_to_output use_infix_notation i in
   let _ = if is_infix_pos && not (List.length args = 2) then (raise (Reporting_basic.err_unreachable false Ast.Unknown "Infix position with wrong number of args")) else () in
 
   let c_descr = c_env_lookup Ast.Unknown A.env.c_env c_id.descr in
-  match Target.Targetmap.apply_opt c_descr.target_rep A.target_opt with
+  match Target.Targetmap.apply_target c_descr.target_rep A.target with
      | Some (CR_special (_, _, _, _, to_out, vars)) -> 
             if (List.length args < List.length vars) then begin
               raise (Reporting_basic.err_todo true Ast.Unknown "Special function syntax needs fun-introduction!")
 
 let pattern_application_to_output (arg_f : pat -> Output.t) (c_id : const_descr_ref id) (args : pat list) : Output.t list =
   let c_descr = c_env_lookup Ast.Unknown A.env.c_env c_id.descr in
-  match Target.Targetmap.apply_opt c_descr.target_rep A.target_opt with
+  match Target.Targetmap.apply_target c_descr.target_rep A.target with
      | Some (CR_special (_, _, _, _, to_out, vars)) -> 
         if (List.length args < List.length vars) then begin
            raise (Reporting_basic.err_unreachable true Ast.Unknown "Constructor without enough arguments!")
 let type_path_to_name n0 (p : Path.t) : Name.lskips_t =
   let l = Ast.Trans ("type_path_to_name", None) in
   let td = Types.type_defs_lookup l A.env.t_env p in
-  let n = type_descr_to_name A.target_opt p td in
+  let n = type_descr_to_name A.target p td in
   let n' = Name.replace_lskip (Name.add_lskip n) (Name.get_lskip n0) in
   n'
 
 let type_id_to_ident (p : Path.t id) =
    let l = Ast.Trans ("type_id_to_ident", None) in
    let td = Types.type_defs_lookup l A.env.t_env p.descr in
-   match Target.Targetmap.apply_opt td.Types.type_target_rep A.target_opt with
+   match Target.Targetmap.apply_target td.Types.type_target_rep A.target with
      | None -> resolve_ident_path p p.descr
      | Some (Types.TR_new_ident (_, _, i)) -> i 
      | Some (Types.TR_rename (_, _, n)) -> Ident.rename (resolve_ident_path p p.descr) n
 let const_ref_to_name n0 c =
   let l = Ast.Trans ("const_ref_to_name", None) in
   let c_descr = c_env_lookup l A.env.c_env c in
-  let (_, n) = constant_descr_to_name A.target_opt c_descr in
+  let (_, n) = constant_descr_to_name A.target c_descr in
   let n' = Name.replace_lskip (Name.add_lskip n) (Name.get_lskip n0) in
   n'
 

src/backend_common.mli

 
 open Typed_ast
 
-(** [inline_exp_macro target_opt env e] does the inlining of target specific constant definitions *)
-val inline_exp_macro : Target.target option -> env -> exp -> exp option
+(** [inline_exp_macro target env e] does the inlining of target specific constant definitions *)
+val inline_exp_macro : Target.non_ident_target -> env -> exp -> exp option
 
 
 module Make(A : sig
   val env : env;; 
-  val target_opt : Target.target option;;
+  val target : Target.target;;
   val id_format_args : (Output.id_annot -> Ulib.Text.t -> Output.t) * Output.t
  end) : sig
 
 val pattern_application_to_output : (pat -> Output.t) -> const_descr_ref id -> pat list -> Output.t list
 
 (** [const_id_to_ident c_id] tries to format a constant
-    [c_id] as an identifier for target [A.target_opt] using the rules stored
+    [c_id] as an identifier for target [A.target] using the rules stored
     in environment [A.env]. Depending on the formating rules for this
     constant, this might fail. *)
 val const_id_to_ident : const_descr_ref id -> Ident.t
 
 (** [const_ref_to_name n c] tries to format a constant
-    [c] for target [A.target_opt] using the rules stored
+    [c] for target [A.target] using the rules stored
     in environment [A.env]. It always returns a name [n']. If special formatting
     rules are installed, this name might not be the one used by [function_application_to_output], though.
     The argument [n] is the name used in the original input. It's whitespace is used to
 val const_ref_to_name : Name.lskips_t -> const_descr_ref -> Name.lskips_t
 
 (** [type_path_to_name n p] tries to format a type-path
-    [p] for target [A.target_opt] using the rules stored
+    [p] for target [A.target] using the rules stored
     in environment [A.env]. It always returns a name [n']. If special formatting
     rules are installed, this name might not be the one used by [function_application_to_output], though.
     The argument [n] is the name used in the original input. It's whitespace is used to
 val type_path_to_name : Name.lskips_t -> Path.t -> Name.lskips_t
 
 (** [type_id_to_ident ty_id] tries to format a type
-    [c_id] as an identifier for target [A.target_opt] using the rules stored
+    [c_id] as an identifier for target [A.target] using the rules stored
     in environment [A.env]. 
 *)
 val type_id_to_ident : Path.t id -> Ident.t

src/coq_backend.ml

       	not d1 && not d2 && s1 = s2
 ;;
 
-let in_target targets = Typed_ast.in_targets_opt (Some Target.Target_coq) targets;;
+let in_target targets = Typed_ast.in_targets_opt (Target.Target_no_ident Target.Target_coq) targets;;
 
 let coq_infix_op a x =
   Output.flat [
     module B = Backend_common.Make (
       struct
         let env = A.env
-        let target_opt = Some Target_coq
+        let target = Target_no_ident Target_coq
         let id_format_args = (coq_infix_op, path_sep)
       end);;
 
   (* def_walker walks over a list of definitions, checks for each def if it is a 
    * target specific one, in which case it invokes rem_dups with both, the
    * already checked defs and the remaining defs *)
-  let rec def_walker (target : Target.target) acc =  function
+  let rec def_walker (target : Target.non_ident_target) acc =  function
     | [] -> List.rev acc
 
     | ((def,s),l)::defs -> begin
           Val_def(Fun_def(_,_,topt,_),_,_) |
           Indreln(_,topt,_) ) as d -> 
 
-          if Typed_ast.in_targets_opt (Some target) topt then 
+          if Typed_ast.in_targets_opt (Target_no_ident target) topt then 
               let name = get_name d l in
               let acc' = rem_dups name acc in  
               let defs' = rem_dups name defs in
             def_walker target acc defs
       
        | Lemma(_,lty,targets,_,_,_,_) as d ->
-         let targ_OK = Typed_ast.in_targets_opt (Some target) targets in
+         let targ_OK = Typed_ast.in_targets_opt (Target_no_ident target) targets in
          if (target_supports_lemma_type target lty && targ_OK) then
             def_walker target (((d,s),l) :: acc) defs
          else

src/def_trans.mli

   val class_constraint_to_parameter : def_macro
   val nvar_to_parameter : def_macro
 
-  val prune_target_bindings : Target.target -> def list -> def list
+  val prune_target_bindings : Target.non_ident_target -> def list -> def list
 
 end
 

src/initial_env.ml

           []
   in f()
 
-type t = 
-    Typed_ast.env * (Target.target option * Ulib.Text.t list) list
+type t = Typed_ast.env * (Target.target * Ulib.Text.t list) list
 
 let filename_to_mod file =
   Ulib.Text.of_latin1 (String.capitalize (Filename.basename (Filename.chop_extension file))) 
 let process_lib target file mod_name (init_env : Typed_ast.env) =
   let mp = 
     match target with
-      | None -> []
-      | Some(n) -> [(target_to_mname n)]
+      | Target_ident -> []
+      | Target_no_ident n -> [(non_ident_target_to_mname n)]
   in
   let ast = parse_file file in
   let (new_defs,_) =
   in
   let new_defs2 =
     match target with
-      | None -> new_defs
-      | Some(tgt) -> 
+      | Target_ident -> new_defs
+      | Target_no_ident (tgt) -> 
         let (c_env', local_env') = add_target_to_def tgt new_defs.c_env new_defs.local_env in
         {new_defs with c_env = c_env'; local_env = local_env'}
   in
         assert false
 
 (* Process a library for the given target and open it in the current init_env *)
-let proc_open target file env =
+let proc_open (target : target) file env =
   let mod_name = filename_to_mod file in
   let new_env = process_lib target file mod_name env in
     (add_open_lib mod_name env.local_env new_env)
 
 (* Process a library for the given target *)
-let proc target file env =
+let proc (target : target) file env =
   let mod_name = filename_to_mod file in
   let new_env = process_lib target file mod_name env in
     (add_lib env.local_env new_env)
 (* TODO: Add to the constants *)
 let add_to_init targ file (((env:env), consts):t) : t =
   let targ_env = 
-    match Nfmap.apply env.local_env.m_env (target_to_mname targ) with 
+    match Nfmap.apply env.local_env.m_env (non_ident_target_to_mname targ) with 
       | Some(e) -> e
       | None -> assert false
   in
       | Target_tex -> assert false
       | Target_html -> assert false
   in
-  let new_env = p (Some targ) file {env with local_env = targ_env.mod_env} in
-    ({ new_env with local_env = {env.local_env with m_env = Nfmap.insert new_env.local_env.m_env (target_to_mname targ, {targ_env with mod_env = new_env.local_env})}}, 
+  let new_env = p (Target_no_ident targ) file {env with local_env = targ_env.mod_env} in
+    ({ new_env with local_env = {env.local_env with m_env = Nfmap.insert new_env.local_env.m_env (non_ident_target_to_mname targ, {targ_env with mod_env = new_env.local_env})}}, 
      consts)
 
 module Initial_libs (P : sig val path : string end) =
   open P
 
   let full_filename targ f = 
-    List.fold_right Filename.concat [path; target_to_string targ] (f ^ ".lem")
+    List.fold_right Filename.concat [path; non_ident_target_to_string targ] (f ^ ".lem")
   ;;
 
   (* HOL Env *)
   let hol_env = 
     List.fold_left
-      (fun init_env t -> proc_open (Some(Target_hol)) (full_filename Target_hol t) init_env)
+      (fun init_env t -> proc_open (Target_no_ident (Target_hol)) (full_filename Target_hol t) init_env)
       initial_env
       ["min"; "bool"; "pair"; "arithmetic"; "pred_set"; "finite_map"; "list"; "string"; "sorting"; "set_relation"; "fixedPoint"; "integer"]
 
-  let hol_env' = env_m_env_move hol_env (target_to_mname Target_hol) initial_local_env
+  let hol_env' = env_m_env_move hol_env (non_ident_target_to_mname Target_hol) initial_local_env
 
 
   (* Coq Env *)
-  let coq_perv = proc_open (Some Target_coq) (full_filename Target_coq "pervasives") hol_env';;
+  let coq_perv = proc_open (Target_no_ident Target_coq) (full_filename Target_coq "pervasives") hol_env';;
 
   let coq_env = 
     List.fold_left (
       fun init_env t ->
-        proc (Some Target_coq) (full_filename Target_coq t) init_env
+        proc (Target_no_ident Target_coq) (full_filename Target_coq t) init_env
     ) coq_perv
     ["pervasives"; "set"; "list"] 
   ;;
   
-  let coq_env' = env_m_env_move coq_env (target_to_mname Target_coq) initial_local_env
+  let coq_env' = env_m_env_move coq_env (non_ident_target_to_mname Target_coq) initial_local_env
   let hol_env' = {coq_env' with local_env = hol_env'.local_env}
 
   (* OCAML Env *)
-  let ocaml_perv = proc_open (Some(Target_ocaml)) (full_filename Target_ocaml "pervasives") hol_env'
+  let ocaml_perv = proc_open (Target_no_ident Target_ocaml) (full_filename Target_ocaml "pervasives") hol_env'
 
   let ocaml_env = 
     List.fold_left
-      (fun init_env t -> proc (Some(Target_ocaml)) (full_filename Target_ocaml t) init_env)
+      (fun init_env t -> proc (Target_no_ident Target_ocaml) (full_filename Target_ocaml t) init_env)
       ocaml_perv
       ["list"; "pset"; "pmap"; "nat_num" ; "vector" ; "bit"]
   
-  let ocaml_env' = env_m_env_move ocaml_env (target_to_mname Target_ocaml) initial_local_env
+  let ocaml_env' = env_m_env_move ocaml_env (non_ident_target_to_mname Target_ocaml) initial_local_env
   let hol_env' = {ocaml_env' with local_env = hol_env'.local_env}
 
   (* Isabelle Env *)
-  let isa_perv = proc_open (Some(Target_isa)) (full_filename Target_isa "pervasives") hol_env'
+  let isa_perv = proc_open (Target_no_ident Target_isa) (full_filename Target_isa "pervasives") hol_env'
 
   let isa_env = 
       List.fold_left
-        (fun init_env t -> proc_open (Some(Target_isa)) (full_filename Target_isa t) init_env)
+        (fun init_env t -> proc_open (Target_no_ident Target_isa) (full_filename Target_isa t) init_env)
         isa_perv
         ["pervasives";"list";"set";"finite_Set";"map"]   
         (* PS HACK - TEMPORARILY REMOVE IN HOPES OF GETTING HOL BUILD *)
   
-  let isa_env' = env_m_env_move isa_env (target_to_mname Target_isa) initial_local_env
+  let isa_env' = env_m_env_move isa_env (non_ident_target_to_mname Target_isa) initial_local_env
 
   let env = {isa_env' with local_env = 
      local_env_union hol_env'.local_env (
                      ocaml_env'.local_env)) }
      
   let perv =
-    proc_open None (Filename.concat path "pervasives.lem") env
+    proc_open Target_ident (Filename.concat path "pervasives.lem") env
   ;;
 
   let env =
      List.fold_left (
-       fun env t -> proc None (Filename.concat path (t ^ ".lem")) env
+       fun env t -> proc Target_ident (Filename.concat path (t ^ ".lem")) env
      ) perv ["list"; "set"; "pmap"; "int" ; "vector" ; "bit"];;
 
   let env = set_target_const_rep env ["Pervasives"] "SUC" Target_isa (CR_new_ident (Ast.Unknown, false, Ident.mk_ident_strings [] "Suc"));;
   let env = set_target_const_rep env ["Pervasives"] "SUC" Target_hol (CR_new_ident (Ast.Unknown, false, Ident.mk_ident_strings [] "SUC"));;
 
-  let init =
+  let init : t =
     (env,
-     [(Some(Target_hol),
-       read_constants (path ^^ target_to_string Target_hol ^^ "constants"));
-      (Some(Target_isa),
-       read_constants (path ^^ target_to_string Target_isa ^^ "constants"));
-      (Some(Target_ocaml),
+     [(Target_no_ident Target_hol,
+       read_constants (path ^^ non_ident_target_to_string Target_hol ^^ "constants"));
+      (Target_no_ident Target_isa,
+       read_constants (path ^^ non_ident_target_to_string Target_isa ^^ "constants"));
+      (Target_no_ident Target_ocaml,
        []);
-      (Some(Target_coq),
-       read_constants (path ^^ target_to_string Target_coq ^^ "constants"));
-      (None,
+      (Target_no_ident Target_coq,
+       read_constants (path ^^ non_ident_target_to_string Target_coq ^^ "constants"));
+      (Target_ident,
        []);
-      (Some(Target_tex),
+      (Target_no_ident Target_tex,
        []);
-      (Some(Target_html),
+      (Target_no_ident Target_html,
        [])])
 end

src/initial_env.mli

 
 open Types
 type t = 
-    Typed_ast.env * (Target.target option * Ulib.Text.t list) list
-val add_to_init : Target.target -> string -> t -> t
+    Typed_ast.env * (Target.target * Ulib.Text.t list) list
+val add_to_init : Target.non_ident_target -> string -> t -> t
 
 module Initial_libs(P : sig val path : string end) : sig
   val init : t
 open Process_file
 open Debug
 
-let backends = ref []
+let backends = ref ([] : Target.target list)
+
+let add_backend b () : unit = if not (List.mem b !backends) then (backends := b::!backends)
+
 let opt_print_types = ref false
 let opt_print_version = ref false
 let opt_library = ref (Some (Build_directory.d^"/library"))
     Arg.String (fun l -> lib := l::!lib),
     " treat the file as input only and generate no output for it");
   ( "-tex", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_tex)) !backends) then
-                backends := Some(Target.Target_tex)::!backends),
+    Arg.Unit (add_backend (Target.Target_no_ident Target.Target_tex)),
     " generate LaTeX");
   ( "-html", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_html)) !backends) then
-                backends := Some(Target.Target_html)::!backends),
+    Arg.Unit (add_backend (Target.Target_no_ident Target.Target_html)),
     " generate Html");
   ( "-hol", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_hol)) !backends) then
-                backends := Some(Target.Target_hol)::!backends),
+    Arg.Unit (add_backend (Target.Target_no_ident Target.Target_hol)),
     " generate HOL");
   ( "-ocaml", 
-    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_ocaml)) !backends) then
-                backends := Some(Target.Target_ocaml)::!backends),
+    Arg.Unit (add_backend (Target.Target_no_ident Target.Target_ocaml)),
     " generate OCaml");
   ( "-isa",
-    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_isa)) !backends) then
-                backends := Some(Target.Target_isa)::!backends),
+    Arg.Unit (add_backend (Target.Target_no_ident Target.Target_isa)),
     " generate Isabelle");
   ( "-coq",
-    Arg.Unit (fun b -> if not (List.mem (Some(Target.Target_coq)) !backends) then
-                backends := Some(Target.Target_coq)::!backends),
+    Arg.Unit (add_backend (Target.Target_no_ident Target.Target_coq)),
     " generate Coq");
   ( "-ident",
-    Arg.Unit (fun b -> if not (List.mem None !backends) then
-                backends := None::!backends),
+    Arg.Unit (add_backend Target.Target_ident),
     " generate input on stdout");
   ( "-print_types",
     Arg.Unit (fun b -> opt_print_types := true),
          let backend_set = 
            List.fold_right 
              (fun x s ->
-                match x with
+                match Target.dest_human_target x with
                   | None -> s
-                  | Some(Target.Target_tex) -> s
-                  | Some(Target.Target_html) -> s
                   | Some(t) -> Target.Targetset.add t s)
              !backends
              Target.Targetset.empty 
   let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in
   let _ = List.fold_left (fun env -> (per_target lib_path isa_thy (List.rev modules) env consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum))
     type_info !backends in
-  (if List.mem (Some(Target.Target_tex)) !backends then 
+  (if List.mem (Target.Target_no_ident Target.Target_tex) !backends then 
      output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)
 
 let _ = 
     (fun _   -> record_matrix_compile_fun)]
 
 (* Target specific ones, use [basic_compile_funs] as a fallback. *)
-let get_target_compile_funs (topt:target option) : (bool -> env -> var_name_generator -> Types.t -> Ast.l -> matrix_compile_fun) list = 
+let get_target_compile_funs (topt:target) : (bool -> env -> var_name_generator -> Types.t -> Ast.l -> matrix_compile_fun) list = 
   let rec target_compile_funs topt =
     match topt with
-    | Some Target_ocaml -> [
+    | Target_no_ident Target_ocaml -> [
          (fun _   -> num_add_matrix_compile_fun true (fun i -> i < 3)); (* if less than 3 cases are missing list all cases, otherwise use >= *)
          (fun _   -> num_matrix_compile_fun true);
       ]
-    | Some Target_hol -> [
+    | Target_no_ident Target_hol -> [
          (fun _ _ -> bool_matrix_compile_fun true); 
          (fun _   -> string_matrix_compile_fun true); 
          (fun _   -> num_matrix_compile_fun true);
       ]
-    | Some Target_isa -> [
+    | Target_no_ident Target_isa -> [
          (fun _   -> num_matrix_compile_fun true);
       ]
-    | Some Target_coq -> [
+    | Target_no_ident Target_coq -> [
          (fun _   -> num_matrix_compile_fun true);
       ]
-    | None -> (* make identity behave like ocaml for debug *) target_compile_funs (Some Target_ocaml)
+    | Target_ident -> (* make identity behave like ocaml for debug, controlled by flag !ident_force_pattern_compile *) target_compile_funs (Target_no_ident Target_ocaml) 
     | _ -> []
   in target_compile_funs topt @ basic_compile_funs
 
     the whole case-expression is processed and transformed into an expression with
     the same semantics that contains only supported patterns. During this compilation, 
     warning messages might be issued. This warning uses [target_opt]. Otherwise, it is not used.*)
-val compile_match_exp : target option -> match_check_arg -> env -> exp -> exp option
+val compile_match_exp : target -> match_check_arg -> env -> exp -> exp option
 
-val compile_exp : target option -> match_check_arg -> Types.type_defs -> env -> exp -> exp option
+val compile_exp : target -> match_check_arg -> Types.type_defs -> env -> exp -> exp option
 
-val compile_def : target option -> match_check_arg -> env -> Def_trans.def_macro
+val compile_def : target -> match_check_arg -> env -> Def_trans.def_macro
 
 
 val is_isabelle_pattern_match : match_check_arg
 
 (** [remove_toplevel_match] tries to introduce matching directly in the function definition by
     eliminating match-expressions in the body. *)
-val remove_toplevel_match : target option -> match_check_arg -> env -> Def_trans.def_macro
+val remove_toplevel_match : target -> match_check_arg -> env -> Def_trans.def_macro
 
 (** [collapse_nested_matches] tries to eliminate nested matches by collapsing them. It is used internally by pattern
     compilation. *)

src/precedence.ml

     | (Pcons_right,_) -> false
 
 
-let get_prec target_opt env c =
+let get_prec targ env c =
   let l = Ast.Trans ("get_prec", None) in
   let c_descr = c_env_lookup l env.c_env c in
 
-(* TODO: Use the taregt_rep
+(* TODO: Use the target_rep
   let i = match Target.Targetmap.apply_opt c_descr.target_rep target_opt with
      | None -> resolve_ident_path c_id c_descr.const_binding
      | Some (CR_new_ident i) -> i
 *)
   
   let n = Path.get_name c_descr.const_binding in
-  let p_fun = match target_opt with 
-    | Some Target.Target_ocaml -> get_prec_ocaml
-    | Some Target.Target_hol -> get_prec_hol
-    | Some Target.Target_isa -> get_prec_isa
+  let p_fun = match targ with 
+    | Target.Target_no_ident Target.Target_ocaml -> get_prec_ocaml
+    | Target.Target_no_ident Target.Target_hol -> get_prec_hol
+    | Target.Target_no_ident Target.Target_isa -> get_prec_isa
     | _ -> get_prec
   in
   p_fun (Op (Name.to_string n))

src/precedence.mli

 val needs_parens : context -> exp_kind -> bool
 val pat_needs_parens : pat_context -> pat_kind -> bool
 
-(** [get_prec target_opt env c] looks up the precedence of constant [c] in environment [env]
-    for the target [target_opt]. *)
-val get_prec : Target.target option -> Typed_ast.env -> Typed_ast.const_descr_ref -> t
+(** [get_prec target env c] looks up the precedence of constant [c] in environment [env]
+    for the target [target]. *)
+val get_prec : Target.target -> Typed_ast.env -> Typed_ast.const_descr_ref -> t

src/process_file.ml

 "  </body>\n" ^
 "</html>\n"
 
-let output1 env libpath isa_thy targ avoid m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
+let output1 env libpath isa_thy (targ : Target.target) avoid m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
   let module C = struct
     let avoid = avoid
     let env = env
   let open Typed_ast in
   let f' = Filename.basename (Filename.chop_extension m.filename) in
     match targ with
-      | None ->
+      | Target.Target_ident ->
           let r = B.ident_defs m.typed_ast in
             Printf.printf "%s" (Ulib.Text.to_string r)
-      | Some(Target.Target_html) -> 
+      | Target.Target_no_ident (Target.Target_html) -> 
           begin
             let r = B.html_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".html") in
               Printf.fprintf o "%s" html_postamble;
               close_output_with_check ext_o
           end
-      | Some(Target.Target_hol) ->
+      | Target.Target_no_ident (Target.Target_hol) ->
           begin
             let (r_main, r_extra_opt) = B.hol_defs m.typed_ast in
             let hol_header o = begin
                 close_output_with_check ext_o
               end in ()
           end
-      | Some(Target.Target_tex) -> 
+      | Target.Target_no_ident (Target.Target_tex) -> 
           begin
             let rr = B.tex_defs m.typed_ast in
             (* complete tex document, wrapped in tex_preamble and tex_postamble *)
                     Printf.fprintf o "%s" (Ulib.Text.to_string r_usage);
                     close_output_with_check ext_o
           end
-      | Some(Target.Target_ocaml) -> 
+      | Target.Target_no_ident(Target.Target_ocaml) -> 
           begin
             let (r_main, r_extra_opt) = B.ocaml_defs m.typed_ast in
             let _ = begin
                 close_output_with_check ext_o
              end in ()
           end
-      | Some(Target.Target_isa) -> 
+      | Target.Target_no_ident(Target.Target_isa) -> 
           begin
           try begin
             let (r_main, r_extra_opt) = B.isa_defs m.typed_ast in
                     raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans_header (l, msg)))
           end
 
-      | Some(Target.Target_coq) -> 
+      | Target.Target_no_ident(Target.Target_coq) -> 
           begin
             let r = B.coq_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".v") in
               close_output_with_check ext_o
           end
 
-let output libpath isa_thy targ consts env mods alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
+let output libpath isa_thy (targ : Target.target) consts env mods alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
   List.iter
     (fun m ->
        output1 env libpath isa_thy targ consts m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)

src/process_file.mli

 val output :   
   string ->                           (* The path to the library *)
   string ->                           (* Isabelle Theory to be included *)
-  target option ->                    (* Backend name (None for the identity backend) *) 
+  target ->                           (* Backend name *) 
   Typed_ast.var_avoid_f ->
   Typed_ast.env ->                    (* The full environment built after all typechecking, and transforming *)
   checked_module list ->              (* The typechecked modules *)

src/rename_top_level.ml

     | Nk_module _     -> Name.capitalize n
     | Nk_class        -> None
 
-let compute_target_rename_constant_fun (targ : Target.target option) (nk : name_kind) (n : Name.t) : Name.t option =
+let compute_target_rename_constant_fun (targ : Target.non_ident_target) (nk : name_kind) (n : Name.t) : Name.t option =
   match targ with 
-    | Some Target_ocaml -> compute_ocaml_rename_constant_fun nk n
+    | Target_ocaml -> compute_ocaml_rename_constant_fun nk n
     | _ -> None
 
 let get_fresh_name consts consts' n = 
   if (is_good n) then None else
   Some (Name.fresh (Name.to_rope n) is_good)
 
-let rename_constant (targ : Target.target option) (consts : NameSet.t) (consts_new : NameSet.t) (env : env) (c : const_descr_ref) : 
+let rename_constant (targ : Target.non_ident_target) (consts : NameSet.t) (consts_new : NameSet.t) (env : env) (c : const_descr_ref) : 
   (NameSet.t * env) = begin
   let l = Ast.Trans ("rename_constant", None) in
   let c_d = c_env_lookup l env.c_env c in
-  let (n_is_shown, n) = constant_descr_to_name targ c_d in
+  let (n_is_shown, n) = constant_descr_to_name (Target_no_ident targ) c_d in
 
   (* if constant name is not printed (e.g. for some special syntax, don't rename it *)
   if (not n_is_shown) then (consts_new, env) else
           (* print warning *)
           let n0 : string = Name.to_string (Path.get_name c_d.const_binding) in
           let _ = (if (not is_auto_renamed) then () else 
-                  (Reporting.report_warning env (Reporting.Warn_rename (c_d.spec_l, n0, Util.option_map (fun (l, n) -> (Name.to_string n, l)) via_opt, Name.to_string n'', targ))))
+                  (Reporting.report_warning env (Reporting.Warn_rename (c_d.spec_l, n0, Util.option_map (fun (l, n) -> (Name.to_string n, l)) via_opt, Name.to_string n'', Target_no_ident targ))))
           in
 
           (* update environment *)
   end
 end
 
-let rename_type (targ : Target.target option) (consts : NameSet.t) (consts_new : NameSet.t) (env : env) (t : Path.t) : 
+let rename_type (targ : Target.non_ident_target) (consts : NameSet.t) (consts_new : NameSet.t) (env : env) (t : Path.t) : 
   (NameSet.t * env) = begin
   let l = Ast.Trans ("rename_type", None) in
   let td = Types.type_defs_lookup l env.t_env t in
-  let n = type_descr_to_name targ t td in
+  let n = type_descr_to_name (Target_no_ident targ) t td in
 
   (* apply target specific renaming *)
   let n'_opt = compute_target_rename_constant_fun targ (Nk_typeconstr t) n in
           (* print warning *)
           let n0 : string = Name.to_string (Path.get_name t) in
           let _ = (if (not is_auto_renamed) then () else 
-                  (Reporting.report_warning env (Reporting.Warn_rename (Ast.Unknown, n0, Util.option_map (fun (l, n) -> (Name.to_string n, l)) via_opt, Name.to_string n'', targ))))
+                  (Reporting.report_warning env (Reporting.Warn_rename (Ast.Unknown, n0, Util.option_map (fun (l, n) -> (Name.to_string n, l)) via_opt, Name.to_string n'', Target_no_ident targ))))
           in
 
           (* update environment *)
 end
 
 
-let rename_defs_target targ ue consts env = 
-  match targ with (* do nothing for identity backend *) None -> env | _ -> 
+let rename_defs_target (targ : Target.target) ue consts env = 
+  match targ with
+    | Target_ident -> env
+    | Target_no_ident targ_ni ->
   begin 
-    let (new_types', env) = List.fold_left (fun (consts_new, env) t -> rename_type targ consts consts_new env t) (NameSet.empty, env) 
+    let (new_types', env) = List.fold_left (fun (consts_new, env) t -> rename_type targ_ni consts consts_new env t) (NameSet.empty, env) 
       ue.Typed_ast_syntax.used_types in
 
 
     (* rename constants *)
-    let (new_consts', env) = List.fold_left (fun (consts_new, env) c -> rename_constant targ consts consts_new env c) (NameSet.empty, env) 
+    let (new_consts', env) = List.fold_left (fun (consts_new, env) c -> rename_constant targ_ni consts consts_new env c) (NameSet.empty, env) 
       ue.Typed_ast_syntax.used_consts in
     env
   end

src/rename_top_level.mli

 (** [rename_target topt ue consts e] processes the entities (constants, constructors, types, modules ...) stored in [ue] and
     renames them for target [topt]. This renaming is target specific. It avoids the names in set [consts] and modifies the descriptions
     of constants, types, etc. in environment [e]. The modified environment is returned. *)
-val rename_defs_target : Target.target option -> Typed_ast_syntax.used_entities -> Typed_ast.NameSet.t -> Typed_ast.env -> Typed_ast.env
+val rename_defs_target : Target.target -> Typed_ast_syntax.used_entities -> Typed_ast.NameSet.t -> Typed_ast.env -> Typed_ast.env
 
   
 type warning = 
   | Warn_general of bool * Ast.l * string
-  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Target.target option
+  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Target.target 
   | Warn_pattern_compilation_failed of Ast.l * Typed_ast.pat list * warn_source
   | Warn_pattern_not_exhaustive of Ast.l * Typed_ast.pat list list
   | Warn_def_not_exhaustive of Ast.l * string * Typed_ast.pat list list
   | Warn_pattern_redundant of Ast.l * (int * Typed_ast.pat) list * Typed_ast.exp
   | Warn_def_redundant of Ast.l * string * (int * Typed_ast.pat) list * Typed_ast.def
-  | Warn_pattern_needs_compilation of Ast.l * Target.target option * Typed_ast.exp * Typed_ast.exp
+  | Warn_pattern_needs_compilation of Ast.l * Target.target * Typed_ast.exp * Typed_ast.exp
   | Warn_unused_vars of Ast.l * string list * warn_source
-  | Warn_fun_clauses_resorted of Ast.l * Target.target option * string list * Typed_ast.def
+  | Warn_fun_clauses_resorted of Ast.l * Target.target * string list * Typed_ast.def
   | Warn_record_resorted of Ast.l * Typed_ast.exp
   | Warn_no_decidable_equality of Ast.l * string
 
   | Warn_general (b, l, m) -> Some (b, l, m)
 
   | Warn_rename (l, n_org, n_via_opt, n_new, targ) ->
-     let target_s = (Target.target_opt_to_string targ) in
+     let target_s = (Target.target_to_string targ) in
      let via_s = (Util.option_default "" (Util.option_map (fun (n, l') -> "\n  via '"^n^"' at " ^
                   loc_to_string true l') n_via_opt)) in
      let m = Format.sprintf "renaming '%s' to '%s' for target %s%s" n_org n_new target_s via_s in
       Some (true, l, m)
 
   | Warn_pattern_needs_compilation (l, targ, e_old, e_new) -> 
-      let target_s = Target.target_opt_to_string targ in
+      let target_s = Target.target_to_string targ in
       let m_basic = "pattern compilation used for target " ^ target_s in
       let m_verb = if not verbose then "" else begin
         let e_old_s = Ulib.Text.to_string (B.ident_exp e_old) in
       let fun_label = if List.length nl > 1 then "functions " else "function " in
       let fsL = List.map (fun s -> ("'" ^ s ^ "'")) nl in
       let fs = String.concat ", " fsL in
-      let target_s = Target.target_opt_to_string targ in
+      let target_s = Target.target_to_string targ in
       let m : string = Format.sprintf "function definition clauses of %s %s reordered for target %s" fun_label fs target_s in
       Some (false, l, m)
 

src/reporting.mli

   | Warn_general of bool * Ast.l * string
     (** [Warn_general vl ls m] is a general warning with message [m], locations [ls] and a flag [vl] whether to print these locations verbosely. *)
 
-  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Target.target option 
+  | Warn_rename of Ast.l * string * (string * Ast.l) option * string * Target.target 
     (** Warning about renaming an identifier. The arguments are the old name, an optional intermediate one, the new name and the target *)
 
   | Warn_pattern_compilation_failed of Ast.l * Typed_ast.pat list * warn_source 
   | Warn_def_redundant of Ast.l * string * (int * Typed_ast.pat) list * Typed_ast.def 
     (** redundant patterns in function definition *)
 
-  | Warn_pattern_needs_compilation of Ast.l * Target.target option * Typed_ast.exp * Typed_ast.exp 
+  | Warn_pattern_needs_compilation of Ast.l * Target.target * Typed_ast.exp * Typed_ast.exp 
     (** [Warn_pattern_needs_compilation l topt old_e new_e] warns about the compilation of [old_e] to [new_e] for target [topt] *)
 
   | Warn_unused_vars of Ast.l * string list * warn_source 
     (** unused variables detected *)
 
-  | Warn_fun_clauses_resorted of Ast.l * Target.target option * string list * Typed_ast.def 
+  | Warn_fun_clauses_resorted of Ast.l * Target.target * string list * Typed_ast.def 
     (** clauses of mutually recursive function definitions resorted *)
 
   | Warn_record_resorted of Ast.l * Typed_ast.exp
 
 let r = Ulib.Text.of_latin1
 
-type target = 
+type non_ident_target = 
   | Target_hol
   | Target_ocaml
   | Target_isa
   | Target_tex
   | Target_html
 
+type target =
+  | Target_no_ident of non_ident_target 
+  | Target_ident
+
 let all_targets_list = [
   Target_hol; 
   Target_ocaml; 
 
 let ast_target_compare x y = Pervasives.compare (ast_target_to_int x) (ast_target_to_int y)
 
-module Targetmap = Finite_map.Dmap_map(
-struct 
-  type t = target
-  let compare = target_compare
-end)
+module Targetmap = struct 
+
+  (* include finite maps *)
+  include Finite_map.Fmap_map(
+    struct 
+      type t = non_ident_target
+      let compare = target_compare
+    end
+  )
+
+  let apply_target m targ = 
+    match targ with
+      | Target_ident -> None (* No entry for identity backend *)
+      | Target_no_ident t -> apply m t
+
+end
 
 module Targetset = Set.Make(
 struct 
-  type t = target
+  type t = non_ident_target
   let compare = target_compare
 end)
 
 let all_targets = List.fold_right Targetset.add all_targets_list Targetset.empty
 
-let target_to_string = function
+let non_ident_target_to_string = function
   | Target_hol -> "hol"
   | Target_ocaml -> "ocaml"
   | Target_isa -> "isabelle"
   | Target_tex -> "tex"
   | Target_html -> "html"
 
-let target_opt_to_string = function
-  | None -> "ident"
-  | Some t -> target_to_string t
+let target_to_string = function
+  | Target_ident -> "ident"
+  | Target_no_ident t -> non_ident_target_to_string t
 
 let target_to_output a t = 
   let open Output in
       | Ast.Target_tex(s) -> ws s ^ id a (r"tex")
       | Ast.Target_html(s) -> ws s ^ id a (r"html")
 
-let target_to_mname = function
+let non_ident_target_to_mname = function
   | Target_hol -> Name.from_rope (r"Hol")
   | Target_ocaml -> Name.from_rope (r"Ocaml")
   | Target_isa -> Name.from_rope (r"Isabelle")
   | Target_tex -> Name.from_rope (r"Tex")
   | Target_html -> Name.from_rope (r"Html")
 
+
+let is_human_target = function
+    Target_ident -> true
+  | Target_no_ident Target_isa   -> false
+  | Target_no_ident Target_hol   -> false
+  | Target_no_ident Target_coq   -> false
+  | Target_no_ident Target_ocaml -> false
+  | Target_no_ident Target_html  -> true
+  | Target_no_ident Target_tex   -> true
+
+
+let dest_human_target = function
+    Target_ident -> None
+  | Target_no_ident t ->  if is_human_target (Target_no_ident t) then None else Some t
 
 (** A datatype for Targets. In contrast to the one in
     [ast.ml] this one does not carry white-space information. *)
-type target = 
+type non_ident_target = 
   | Target_hol
   | Target_ocaml
   | Target_isa
   | Target_tex
   | Target_html
 
+(** [target] for the typechecked ast is either a real target as in the AST or
+    the identity target *)
+type target =
+  | Target_no_ident of non_ident_target 
+  | Target_ident
+
 (** [ast_target_to_target t] converts an ast-target to a
     target. This essentially means dropping the white-space information. *)
-val ast_target_to_target : Ast.target -> target
+val ast_target_to_target : Ast.target -> non_ident_target
 
 (** [target_to_ast_target t] converts a target [t] to an
     ast_target. This essentially means adding empty white-space information. *)
-val target_to_ast_target : target -> Ast.target
+val target_to_ast_target : non_ident_target -> Ast.target
 
 (** [ast_target_compare] is a comparison function for ast-targets. *)
 val ast_target_compare : Ast.target -> Ast.target -> int
 
 (** [target_compare] is a comparison function for targets. *)
-val target_compare : target -> target -> int
+val target_compare : non_ident_target -> non_ident_target -> int
+
+(** target keyed finite maps *)
+module Targetmap : sig
+   include Finite_map.Fmap with type k = non_ident_target
 
-(** target keyed finite maps with a default value*)
-module Targetmap : Finite_map.Dmap with type k = target
+   (** [apply_drop_ident m targ] looks up the [targ] in map [m]. 
+       Target-maps only store information for real targets, not the identity one.
+       If therefore [targ_opt] is [Target_ident], i.e. represents the identity backend,
+       [None] is returned. *)
+   val apply_target : 'a t -> target -> 'a option
+end
 
 (** target sets *)
-module Targetset : Set.S with type elt = target
+module Targetset : Set.S with type elt = non_ident_target
 
 (** A list of all the targets. *)
-val all_targets_list : target list
+val all_targets_list : non_ident_target list
 
 (** The set of all the targets. *)
 val all_targets : Targetset.t
 
-(** [target_to_string t] returns a string description of a target [t]. *)
-val target_to_string : target -> string
+(** [non_ident_target_to_string t] returns a string description of a target [t]. *)
+val non_ident_target_to_string : non_ident_target -> string
 
-(** [target_opt_to_string t_opt] returns a string description of a target.
+(** [target_to_string t_opt] returns a string description of a target.
     If some target is given, it does the same as [target_to_string]. Otherwise,
     it returns a string description of the identity backend. *)
-val target_opt_to_string : target option -> string
+val target_to_string : target -> string
 
-(** [target_to_mname t] returns a name for a target. It is similar to
-    [target_to_string t]. However, it returns capitalised versions. *)
-val target_to_mname : target -> Name.t
+(** [non_ident_target_to_mname t] returns a name for a target. It is similar to
+    [non_ident_target_to_string t]. However, it returns capitalised versions. *)
+val non_ident_target_to_mname : non_ident_target -> Name.t
 
 (** [target_to_output a t] returns output for a target [t] and id-annotation [a]. *)
 val target_to_output : Output.id_annot -> Ast.target -> Output.t
+
+(** [is_human_target targ] checks whether [targ] is a target intended to be read by humans
+    and therefore needs preserving the original structure very closely. Examples for such targets are
+    the tex-, html- and identity-targets. *)
+val is_human_target : target -> bool
+
+(** [dest_human_target targ] destructs [targ] to get the non-identity target. If it s a human-target, 
+    [None] is returned, otherwise the non-identity target. *)
+val dest_human_target : target -> non_ident_target option

src/target_binding.ml

 module P = Precedence
 
 (* TODO: This needs to be much more complex to be really right *)
-let id_fix_binding target id =
+let id_fix_binding (target : Target.non_ident_target) id =
   match id.id_path with
     | Id_none _ -> id
     | Id_some p -> 
-        { id with id_path = Id_some (Ident.strip_path target p) }
+        { id with id_path = Id_some (Ident.strip_path (Target.non_ident_target_to_mname target) p) }
 
-let rec fix_src_t target t =
+let rec fix_src_t (target : Target.non_ident_target) t =
   match t.term with
     | Typ_wild _ | Typ_var _ -> t
     | Typ_fn(t1,sk,t2) -> 
         { t with term = Typ_paren(sk1, fix_src_t target t', sk2) }
 
 
-let rec fix_pat target p = 
+let rec fix_pat (target : Target.non_ident_target) p = 
   let old_t = Some(p.typ) in
   let old_l = p.locn in
   let trans = fix_pat target in
         n (List.map (fix_pat target) ps) t s1 
         (fix_exp target e)
 
-let rec fix_binding target defs =
+let rec fix_binding (target : Target.non_ident_target) defs =
   let fix_val_def = function
     | Let_def(s1,targets,(p,name_map,t,s2,e)) ->
         Let_def(s1, targets,

src/target_binding.mli

 
 (** try to fix problems from target's different binding *)
 
-val fix_binding : Name.t -> Typed_ast.def list -> Typed_ast.def list
+val fix_binding : Target.non_ident_target -> Typed_ast.def list -> Typed_ast.def list

src/target_syntax.mli

 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-val fix_infix_and_parens : Typed_ast.env -> Target.target option -> Typed_ast.def list -> Typed_ast.def list
+val fix_infix_and_parens : Typed_ast.env -> Target.target -> Typed_ast.def list -> Typed_ast.def list

src/target_trans.ml

 
   let ident =
     { (* for debugging pattern compilation *)
-      macros = [ Def_macros (fun env -> if !ident_force_pattern_compile then [Patterns.compile_def None (Patterns.is_pattern_match_const false) env] else []);
-                 Exp_macros (fun env -> if !ident_force_pattern_compile then [Patterns.compile_exp None (Patterns.is_pattern_match_const false) C.d env] else []) ];
+      macros = [ Def_macros (fun env -> if !ident_force_pattern_compile then [Patterns.compile_def Target_ident (Patterns.is_pattern_match_const false) env] else []);
+                 Exp_macros (fun env -> if !ident_force_pattern_compile then [Patterns.compile_exp Target_ident (Patterns.is_pattern_match_const false) C.d env] else []) ];
       extra = []; }
 
   let tex =
                                           M.remove_vals;
                                           M.remove_classes; 
                                           M.remove_opens;
-                                          Patterns.compile_def (Some Target_hol) Patterns.is_hol_pattern_match env;]);
+                                          Patterns.compile_def (Target_no_ident Target_hol) Patterns.is_hol_pattern_match env;]);
                 Exp_macros (fun env ->
                               let module T = T(struct let env = env end) in
                                 [T.remove_list_comprehension;
 				 T.remove_setcomp;
                                  T.remove_set_restr_quant;
                                  T.remove_restr_quant Pattern_syntax.is_var_tup_pat;
-                                 Backend_common.inline_exp_macro (Some Target_hol) env;
-                                 Patterns.compile_exp (Some Target_hol) Patterns.is_hol_pattern_match C.d env]);
+                                 Backend_common.inline_exp_macro Target_hol env;
+                                 Patterns.compile_exp (Target_no_ident Target_hol) Patterns.is_hol_pattern_match C.d env]);
                 Pat_macros (fun env ->
                               let module T = T(struct let env = env end) in
                                 [T.peanoize_num_pats])
                [Def_macros (fun env -> let module M = M(struct let env = env end) in 
                               [M.remove_vals; 
                                M.remove_indrelns;
-                               Patterns.compile_def (Some Target_ocaml) Patterns.is_ocaml_pattern_match env]);
+                               Patterns.compile_def (Target_no_ident Target_ocaml) Patterns.is_ocaml_pattern_match env]);
                 Exp_macros (fun env ->
                               let module T = T(struct let env = env end) in
                                 [(* TODO: figure out what it does and perhaps add it again    T.hack; *)
                                  (* TODO: add again or implement otherwise                    T.tup_ctor (fun e -> e) Seplist.empty; *)
-                                 Backend_common.inline_exp_macro (Some Target_ocaml) env;
+                                 Backend_common.inline_exp_macro Target_ocaml env;
                                  T.remove_sets;
                                  T.remove_list_comprehension;
                                  T.remove_quant;
                                  T.remove_vector_access;
                                  T.remove_vector_sub;
                                  T.remove_do;
-                                 Patterns.compile_exp (Some Target_ocaml) Patterns.is_ocaml_pattern_match C.d env])
+                                 Patterns.compile_exp (Target_no_ident Target_ocaml) Patterns.is_ocaml_pattern_match C.d env])
                ];
       extra = [(* (fun n -> Rename_top_level.rename_defs_target (Some Target_ocaml) consts fixed_renames [n]) *)]; 
     }
                       [M.remove_vals;
                        M.remove_opens;
                        M.remove_indrelns_true_lhs;
-                       Patterns.compile_def (Some Target_isa) Patterns.is_isabelle_pattern_match env;] );
+                       Patterns.compile_def (Target_no_ident Target_isa) Patterns.is_isabelle_pattern_match env;] );
         Exp_macros (fun env ->
                       let module T = T(struct let env = env end) in
                         [T.list_quant_to_set_quant;
                          T.remove_set_restr_quant;
                          T.remove_restr_quant Pattern_syntax.is_var_wild_tup_pat;
                          T.remove_set_comp_binding;
-                         Backend_common.inline_exp_macro (Some Target_isa) env;
+                         Backend_common.inline_exp_macro Target_isa env;
                          T.sort_record_fields;
                          T.string_lits_isa;
-                         Patterns.compile_exp (Some Target_isa) Patterns.is_isabelle_pattern_match C.d env]);
+                         Patterns.compile_exp (Target_no_ident Target_isa) Patterns.is_isabelle_pattern_match C.d env]);
         Pat_macros (fun env ->
                       let module T = T(struct let env = env end) in
                         [T.peanoize_num_pats; T.remove_unit_pats])
     { macros =
         [Def_macros (fun env -> let module M = M(struct let env = env end) in 
                       [M.type_annotate_definitions;
-                       Patterns.compile_def (Some Target_coq) Patterns.is_coq_pattern_match env
+                       Patterns.compile_def (Target_no_ident Target_coq) Patterns.is_coq_pattern_match env
                       ]); 
          Exp_macros (fun env -> 
                        let module T = T(struct let env = env end) in
                           T.remove_list_comprehension;
                           T.remove_set_comprehension;
                           T.remove_quant;
-                          Backend_common.inline_exp_macro (Some Target_coq) env;
+                          Backend_common.inline_exp_macro Target_coq env;
                           T.remove_do;
-                          Patterns.compile_exp (Some Target_coq) Patterns.is_coq_pattern_match C.d env]);
+                          Patterns.compile_exp (Target_no_ident Target_coq) Patterns.is_coq_pattern_match C.d env]);
          Pat_macros (fun env ->
                        let module T = T(struct let env = env end) in
                          [T.coq_type_annot_pat_vars])
 
   let get_avoid_f targ : (NameSet.t -> var_avoid_f) = 
     match targ with
-      | Some(Target_ocaml) -> ocaml_avoid_f
-      | Some(Target_isa) -> underscore_avoid_f
-      | Some(Target_hol) -> underscore_avoid_f
-      | Some(Target_coq) -> default_avoid_f true []
+      | Target_no_ident Target_ocaml -> ocaml_avoid_f
+      | Target_no_ident Target_isa -> underscore_avoid_f
+      | Target_no_ident Target_hol -> underscore_avoid_f
+      | Target_no_ident Target_coq -> default_avoid_f true []
       | _ -> default_avoid_f false []
 
   let rename_def_params_aux targ consts =
       List.map (fun (m:Typed_ast.checked_module) -> 
          {m with Typed_ast.typed_ast = (let (defs, end_lex_skips) = m.Typed_ast.typed_ast in (List.map rdp defs, end_lex_skips))})
 
-  let trans targ ttarg params env m =
+  let trans (targ : Target.target) params env m =
     let module Ctxt = struct let avoid = None let env_opt = Some(env) end in
     let module M = Macro_expander.Expander(Ctxt) in
     let (defs, end_lex_skips) = m.typed_ast in
     (* TODO: Move this to a definition macro, and remove the targ argument *)
     let defs =
       match targ with 
-        | None -> defs 
-        | Some(targ) -> let module M2 = Def_trans.Macros(struct let env = env end) in M2.prune_target_bindings targ defs 
+        | Target_ident -> defs
+        | Target_no_ident t -> let module M2 = Def_trans.Macros(struct let env = env end) in M2.prune_target_bindings t defs 
     in
     let (env,defs) = 
       List.fold_left 
         params.extra
     in
     let defs = 
-      match ttarg with
-        | None -> defs
-        | Some(ttarg) ->
-            Target_binding.fix_binding (target_to_mname ttarg) defs 
+      match targ with
+        | Target_ident -> defs
+        | Target_no_ident t -> Target_binding.fix_binding t defs 
     in
-    let defs = Target_syntax.fix_infix_and_parens env ttarg defs in
+    let defs = Target_syntax.fix_infix_and_parens env targ defs in
       (* Note: this is the environment from the macro translations, ignoring the
        * extra translations *)
       (env,
        { m with typed_ast = (List.rev defs, end_lex_skips) })
 
   let get_transformation targ =
-    match targ with
-      | Some(Target_hol) -> 
-          (trans (Some(Target.Target_hol)) targ hol,
-           get_avoid_f targ)
-      | Some(Target_ocaml) -> 
-          (* TODO *)
-          (trans (Some(Target.Target_ocaml)) targ ocaml,
-           get_avoid_f targ)
-      | Some(Target_coq) -> 
-          (trans (Some(Target.Target_coq)) targ coq,
-           get_avoid_f targ)
-      | Some(Target_isa) -> 
-          (trans (Some(Target.Target_isa)) targ isa,
-           get_avoid_f targ)
-      | Some(Target_tex) -> 
-          (trans (Some(Target.Target_tex)) targ tex,
-           get_avoid_f targ)
-      | Some(Target_html) -> 
-          (trans None targ ident,
-           get_avoid_f targ)
-      | None -> 
-          (trans None targ ident,
-           get_avoid_f targ)
+    let tr = match targ with
+      | Target_no_ident Target_hol   -> hol
+      | Target_no_ident Target_ocaml -> ocaml
+      | Target_no_ident Target_coq   -> coq
+      | Target_no_ident Target_isa   -> isa
+      | Target_no_ident Target_tex   -> tex
+      | Target_no_ident Target_html  -> ident
+      | Target_ident                 -> ident
+    in
+      (trans targ tr, get_avoid_f targ)
 
 end

src/target_trans.mli

   (* For each target, returns the (pre-backend) transformation function, and the
   * local variable renaming function (for Typed_ast.Exp_context.avoid) *)
   val get_transformation : 
-    Target.target option -> 
+    Target.target -> 
     ((Typed_ast.env -> Typed_ast.checked_module -> (Typed_ast.env * Typed_ast.checked_module)) *
      (Typed_ast.NameSet.t -> Typed_ast.var_avoid_f))
   
   (* Rename the arguments to definitions, if they clash with constants in a given set of constants.
      This was previously part of the transformation returned by get_transformation. It got moved
      out in order to see all the renamings of definitions before changing their arguments. *)
-  val rename_def_params : Target.target option -> Typed_ast.NameSet.t ->  Typed_ast.checked_module list ->  Typed_ast.checked_module list
+  val rename_def_params : Target.target -> Typed_ast.NameSet.t ->  Typed_ast.checked_module list ->  Typed_ast.checked_module list
 
 (*  (* extend the set of constants that should be avoided, depending on the definitions in
      the modules passed as arguments *)
                                    (fun ppf -> 
                                       Format.fprintf ppf
                                         "unbound variable for targets {%a}"
-                                        (Pp.lst ";" (fun ppf t -> Pp.pp_str ppf (target_to_string t)))
+                                        (Pp.lst ";" (fun ppf t -> Pp.pp_str ppf (non_ident_target_to_string t)))
                                         (Targetset.elements undefined_targets)))
                                 Name.pp (Name.strip_lskip n)
                             else
                            if not (Targetset.is_empty relevant_duplicate_targets) then
                              raise_error l
                                (Printf.sprintf "defined variable already has a %s-specific definition" 
-                                  (target_to_string 
+                                  (non_ident_target_to_string 
                                      (Targetset.choose relevant_duplicate_targets)))
                                Name.pp n 
                  end;
   in
     (v, v_d, ctxt, src_t, (sk1, (n,l'), v, sk2, src_t))
 
-let target_opt_to_set : Ast.targets option -> Targetset.t option = function
+let target_opt_to_set_opt : Ast.targets option -> Targetset.t option = function
   | None -> None
   | Some(Ast.Targets_concrete(_,targs,_)) ->
       Some(List.fold_right
       | Ast.Let_rec(_,_,target_opt,_) -> target_opt
       | Ast.Let_inline (_,_,target_opt,_) ->  target_opt
   in
-  let target_set = target_opt_to_set target_opt_ast in
+  let target_set_opt = target_opt_to_set_opt target_opt_ast in
   let target_opt = check_target_opt target_opt_ast in
-  let env_tag = target_opt_to_env_tag target_set in
+  let env_tag = target_opt_to_env_tag target_set_opt in
 
   let module Checker = Make_checker(T) in
   match vd with
       | Ast.Let_def(sk,_,lb) ->
-          let (lb,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_letbind for_method target_set l lb in 
+          let (lb,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_letbind for_method target_set_opt l lb in 
           let _ = unsat_constraint_err l constraints in
           let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints env_tag e_v in
           let (vd : val_def) = letbind_to_funcl_aux sk target_opt ctxt' lb in
           (ctxt', e_v, vd, Tconstraints(tnvs,constraints,lconstraints))
       | Ast.Let_rec(sk1,sk2,_,funcls) ->
           let funcls = Seplist.from_list funcls in
-          let (lbs,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_funs for_method target_set l funcls in 
+          let (lbs,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_funs for_method target_set_opt l funcls in 
           let _ = unsat_constraint_err l constraints in
           let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints env_tag e_v in
           let fauxs = letbinds_to_funcl_aux_rec l ctxt' lbs in
             (ctxt', e_v, (Fun_def(sk1,Some sk2,target_opt,fauxs)), Tconstraints(tnvs,constraints,lconstraints))
       | Ast.Let_inline (sk1,sk2,_,lb) -> 
-          let (lb,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_letbind for_method target_set l lb in 
+          let (lb,e_v,Tconstraints(tnvs,constraints,lconstraints)) = Checker.check_letbind for_method target_set_opt l lb in 
           let _ = unsat_constraint_err l constraints in
           let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) constraints lconstraints env_tag e_v in
           let (nls, n_ref, _, pL, ty_opt, sk3, et) = letbind_to_funcl_aux_dest ctxt' lb in
                        | Some a -> a in         
           let new_tr = CR_inline (l, args, et) in
           let d = c_env_lookup l ctxt'.c_env n_ref in
-          let tr = match target_set with
-               | None -> Targetmap.set_default d.target_rep (Some new_tr)
-               | Some ts -> Targetset.fold (fun t r -> Targetmap.insert r (t,new_tr)) ts d.target_rep
-            in
+          let ts = Util.option_default Target.all_targets target_set_opt in
+          let tr = Targetset.fold (fun t r -> Targetmap.insert r (t,new_tr)) ts d.target_rep in
           let ctxt'' = {ctxt' with c_env = c_env_update ctxt'.c_env n_ref {d with target_rep = tr}} in
             (ctxt'', e_v, Let_inline(sk1,sk2,target_opt,nls,n_ref,args,sk3,et), Tconstraints(tnvs,constraints,lconstraints))
 
     | None -> None
     | Some target_opt ->
         begin
-          match target_opt_to_set target_opt with
+          match target_opt_to_set_opt target_opt with
             | None -> None
             | Some(ts) -> 
                 Some(Targetset.inter ts backend_targets)
               begin 
                 let cd = c_env_lookup l ctxt.c_env c in
                 let cd' = List.fold_left (fun cd t -> 
-                   match constant_descr_rename (Some t) (Name.strip_lskip n') l cd with
+                   match constant_descr_rename t (Name.strip_lskip n') l cd with
                      | Some (cd', _) -> cd'
                      | None -> raise_error_string l "internal error: count not rename constant. This is a bug and should not happen.")
                    cd (targets_opt_to_list targs) in
           let module T = struct include T let targets = backend_targets end in
           let module Checker = Make_checker(T) in
           let target_opt_checked = check_target_opt target_opt in
-          let target_set = target_opt_to_set target_opt in
+          let target_set_opt = target_opt_to_set_opt target_opt in
           let (cls,e_v,Tconstraints(tnvs,constraints,lconstraints)) = 
-            Checker.check_indrels target_set l clauses in
+            Checker.check_indrels target_set_opt l clauses in
           let ctxt' = add_let_defs_to_ctxt mod_path ctxt (TNset.elements tnvs) 
                constraints lconstraints
-               (target_opt_to_env_tag target_set) e_v in
+               (target_opt_to_env_tag target_set_opt) e_v in
           let add_const (name_opt, s1, qnames, s2, e_opt, s3, rname, es) = begin
               let n = Name.strip_lskip rname.term in
               let n_ref =  match Nfmap.apply ctxt'.cur_env.v_env n with
 
 type targets_opt = (bool * lskips * Ast.target lskips_seplist * lskips) option
 
-let in_targets_opt (t_opt : Target.target option) (targets_opt : targets_opt) : bool = match t_opt with
-    None   -> true
-  | Some t -> (match targets_opt with 
+let in_targets_opt (targ : Target.target) (targets_opt : targets_opt) : bool = match targ with
+    Target_ident   -> true
+  | Target_no_ident t -> (match targets_opt with 
                  None -> true
                | Some (neg, _, targets, _) -> 
                  let is_in = Seplist.exists (fun t' -> ast_target_compare (target_to_ast_target t) t' = 0) targets in
                  if neg then not is_in else is_in)
 
-let targets_opt_to_list (targets_opt : targets_opt) : Target.target list =
-   List.filter (fun t -> in_targets_opt (Some t) targets_opt) Target.all_targets_list
+let targets_opt_to_list (targets_opt : targets_opt) : Target.non_ident_target list =
+   List.filter (fun t -> in_targets_opt (Target_no_ident t) targets_opt) Target.all_targets_list
                          
 
 type val_def = 

src/typed_ast.mli

 type targets_opt = (bool * lskips * Ast.target lskips_seplist * lskips) option
 
 
-(** [in_targets_opt t_opt targets_opt] checks whether the target `t_opt` is in the set of targets represented by
-    `targets_opt`. If `t_opt` is `None`, this represents the identity backend and `true` is returned. *)
-val in_targets_opt : Target.target option -> targets_opt -> bool
+(** [in_targets_opt targ targets_opt] checks whether the target `targ` is in the set of targets represented by
+    `targets_opt`. [targets_opt] contains only AST-targets, i.e. it can't explicitly contain
+     the identity target. If `targ` is the identity backend, `true` is returned for all [targets_opt]. *)
+val in_targets_opt : Target.target -> targets_opt -> bool
 
 (** [target_opt_to_list targets_opt] returns a distinct list of all the targets in the option. *)
-val targets_opt_to_list : targets_opt -> Target.target list
+val targets_opt_to_list : targets_opt -> Target.non_ident_target list
 
 type val_def = 
   | Let_def of lskips * targets_opt * (pat * (Name.t * const_descr_ref) list * (lskips * src_t) option * lskips * exp)

src/typed_ast_syntax.ml

   let new_c_env = c_env_update env.c_env c new_cd in
   {env with c_env = new_c_env}
 
-let constant_descr_to_name (targ : Target.target option) (cd : const_descr) : (bool * Name.t) = 
-  match Target.Targetmap.apply_opt cd.target_rep targ with
+let constant_descr_to_name (targ : Target.target) (cd : const_descr) : (bool * Name.t) = 
+  match Target.Targetmap.apply_target cd.target_rep targ with
     | Some (CR_rename (l, _, n)) -> (true, n)
     | Some (CR_new_ident (_, _, i)) -> (true, Name.strip_lskip (Ident.get_name i))
     | Some (CR_inline _) -> (false, Path.get_name cd.const_binding)
     | Some (CR_special (_, _, b, n, _, _)) -> (b, n)
     | None -> (true, Path.get_name cd.const_binding)
 
-let type_descr_to_name (targ : Target.target option) (p : Path.t) (td : type_descr) : Name.t = 
-  match Target.Targetmap.apply_opt td.Types.type_target_rep targ with
+let type_descr_to_name (targ : Target.target) (p : Path.t) (td : type_descr) : Name.t = 
+  match Target.Targetmap.apply_target td.Types.type_target_rep targ with
      | None -> Path.get_name p 
      | Some (Types.TR_new_ident (_, _, i)) -> Name.strip_lskip (Ident.get_name i)
      | Some (Types.TR_rename (_, _, n)) -> n
 
 
-let constant_descr_rename  (targ : Target.target option) (n':Name.t) (l' : Ast.l) (cd : const_descr) : (const_descr * (Ast.l * Name.t) option) option = 
-  let rep = Target.Targetmap.apply_opt cd.target_rep targ in
+let constant_descr_rename  (targ : Target.non_ident_target) (n':Name.t) (l' : Ast.l) (cd : const_descr) : (const_descr * (Ast.l * Name.t) option) option = 
+  let rep = Target.Targetmap.apply cd.target_rep targ in
   let rep_info_opt = match rep with
     | Some (CR_rename (l, true, n)) -> Some (CR_rename (l', true, n'), Some (l, n))
     | Some (CR_new_ident (l, true, i)) -> Some (CR_new_ident (l', true, Ident.rename i n'), Some (l, Name.strip_lskip (Ident.get_name i)))
     | _ -> None
   in
   let save_env (cr, d) = begin
-    let tr = Target.Targetmap.insert_opt (cd.target_rep) (targ, cr) in
+    let tr = Target.Targetmap.insert (cd.target_rep) (targ, cr) in
     ({cd with target_rep = tr}, d)
   end in
   Util.option_map save_env rep_info_opt
 
-let type_descr_rename  (targ : Target.target option) (n':Name.t) (l' : Ast.l) (td : type_descr) : (type_descr * (Ast.l * Name.t) option) option = 
-  let rep = Target.Targetmap.apply_opt td.type_target_rep targ in
+let type_descr_rename  (targ : Target.non_ident_target) (n':Name.t) (l' : Ast.l) (td : type_descr) : (type_descr * (Ast.l * Name.t) option) option = 
+  let rep = Target.Targetmap.apply td.type_target_rep targ in
   let rep_info_opt = match rep with
     | Some (TR_rename (l, true, n)) -> Some (TR_rename (l', true, n'), Some (l, n))
     | Some (TR_new_ident (l, true, i)) -> Some (TR_new_ident (l', true, Ident.rename i n'), Some (l, Name.strip_lskip (Ident.get_name i)))
     | _ -> None
   in
   let save_env (tr, d) = begin
-    let targ_rep = Target.Targetmap.insert_opt (td.type_target_rep) (targ, tr) in
+    let targ_rep = Target.Targetmap.insert (td.type_target_rep) (targ, tr) in
     ({td with type_target_rep = targ_rep}, d)
   end in
   Util.option_map save_env rep_info_opt
 
-let type_descr_set_ident  (targ : Target.target option) (i:Ident.t) (l' : Ast.l) (td : type_descr) : type_descr option = 
-  let rep = Target.Targetmap.apply_opt td.type_target_rep targ in
+let type_descr_set_ident  (targ : Target.non_ident_target) (i:Ident.t) (l' : Ast.l) (td : type_descr) : type_descr option = 
+  let rep = Target.Targetmap.apply td.type_target_rep targ in
   let rep_info_opt = match rep with
     | (Some (TR_rename (_, true, _)) | Some (TR_new_ident (_, true, _)) | None) -> 
          Some (TR_new_ident (l', true, i))
     | _ -> None
   in
   let save_env tr = begin
-    let targ_rep = Target.Targetmap.insert_opt (td.type_target_rep) (targ, tr) in
+    let targ_rep = Target.Targetmap.insert (td.type_target_rep) (targ, tr) in
     ({td with type_target_rep = targ_rep})
   end in
   Util.option_map save_env rep_info_opt
 
-let type_defs_rename_type l (d : type_defs) (p : Path.t) (t: Target.target) (n : Name.t) : type_defs =
+let type_defs_rename_type l (d : type_defs) (p : Path.t) (t: Target.non_ident_target) (n : Name.t) : type_defs =
   let l' = Ast.Trans ("type_defs_rename_type", Some l) in
   let up td = begin
-    let res_opt = type_descr_rename (Some t) n l td in
+    let res_opt = type_descr_rename t n l td in
     Util.option_map (fun (td, _) -> td) res_opt
   end in
   Types.type_defs_update_tc_type l' d p up
 
-let type_defs_new_ident_type l (d : type_defs) (p : Path.t) (t: Target.target) (i : Ident.t) : type_defs =
+let type_defs_new_ident_type l (d : type_defs) (p : Path.t) (t: Target.non_ident_target) (i : Ident.t) : type_defs =
   let l' = Ast.Trans ("type_defs_target_type", Some l) in
-  let up td = type_descr_set_ident (Some t) i l td in
+  let up td = type_descr_set_ident t i l td in
   Types.type_defs_update_tc_type l' d p up
 
 let const_descr_to_kind (r, d) =
   ue
 end
 
-and add_def_entities (t_opt : Target.target option) (ue : used_entities) (((d, _), _) : def) : used_entities = 
+and add_def_entities (t_opt : Target.target) (ue : used_entities) (((d, _), _) : def) : used_entities = 
   match d with
       | Type_def(sk, tds) ->
          Seplist.fold_left (fun (_, _, type_path, texp, _) ue -> begin
       | Comment _ -> ue
 
 
-let add_checked_module_entities (t_opt : Target.target option) (ue : used_entities) (m : checked_module): used_entities = 
+let add_checked_module_entities (t_opt : Target.target) (ue : used_entities) (m : checked_module): used_entities = 
   let (dl, _) = m.typed_ast in 
   List.fold_left (add_def_entities t_opt) ue dl
 
-let get_checked_modules_entities (t_opt : Target.target option) (ml : checked_module list) : used_entities =
+let get_checked_modules_entities (t_opt : Target.target) (ml : checked_module list) : used_entities =
   reverse_used_entities (List.fold_left (add_checked_module_entities t_opt) empty_used_entities ml)
 
 

src/typed_ast_syntax.mli

 
 (** [set_target_const_rep env mp n target rep] sets the representation of the constant described by
     module-path [mp] and name [n] for target [target] to [rep] in environment [env]. *)
-val set_target_const_rep : env -> string list -> string -> Target.target -> const_target_rep -> env
+val set_target_const_rep : env -> string list -> string -> Target.non_ident_target -> const_target_rep -> env
 
 (** [const_descr_to_name targ cd] looks up the representation for target [targ] in the constant
     description [cd]. It returns a tuple [(n_is_shown, n)]. The name [n] is the name of the constant for this
     target. [n_is_shown] indiciates, whether this name is actually printed. Special representations or inline representation
     might have a name, that is not used for the output. *)
-val constant_descr_to_name : Target.target option -> const_descr -> (bool * Name.t)
+val constant_descr_to_name : Target.target -> const_descr -> (bool * Name.t)
 
 (** [type_descr_to_name targ ty td] looks up the representation for target [targ] in the type
     description [td]. Since in constrast to constant-description, type-descriptions don't contain the
     full type-name, but only renamings, the orginal type-name is passed as argument [ty]. It is assumed that
     [td] really belongs to [ty]. *)
-val type_descr_to_name : Target.target option -> Path.t -> Types.type_descr -> Name.t
+val type_descr_to_name : Target.target -> Path.t -> Types.type_descr -> Name.t
 
 (** [const_descr_rename targ n' l' cd] looks up the representation for target [targ] in the constant
     description [cd]. It then updates this description by renaming to the new name [n'] and new location [l']. 
     If this renaming is not possible, [None] is returned, otherwise the updated description is returned along with information of where the constant
     was last renamed and to which name. *)
-val constant_descr_rename : Target.target option -> Name.t -> Ast.l -> const_descr -> (const_descr * (Ast.l * Name.t) option) option
+val constant_descr_rename : Target.non_ident_target -> Name.t -> Ast.l -> const_descr -> (const_descr * (Ast.l * Name.t) option) option
 
 (** [type_descr_rename targ n' l' td] looks up the representation for target [targ] in the type
     description [td]. It then updates this description by renaming to the new name [n'] and new location [l']. 
     If this renaming is not possible, [None] is returned, otherwise the updated description is returned along with information of where the type
     was last renamed and to which name. *)
-val type_descr_rename : Target.target option -> Name.t -> Ast.l -> Types.type_descr -> (Types.type_descr * (Ast.l * Name.t) option) option
+val type_descr_rename : Target.non_ident_target -> Name.t -> Ast.l -> Types.type_descr -> (Types.type_descr * (Ast.l * Name.t) option) option
 
 (** [type_def_rename_type l d p t n] renames the type with path [p] in the defs [d] to the name [n] for
 target [t]. Renaming means that the module structure is kept. Only the name is changed. *)
-val type_defs_rename_type: Ast.l -> Types.type_defs -> Path.t -> Target.target -> Name.t -> Types.type_defs
+val type_defs_rename_type: Ast.l -> Types.type_defs -> Path.t -> Target.non_ident_target -> Name.t -> Types.type_defs
 
 (** [type_def_new_ident_type l d p t i] changes the representation of the type with path [p] in the defs [d] to the identifier [i] for
 target [t]. This means that the whole module structure is lost and replace by the identifier. *)
-val type_defs_new_ident_type: Ast.l -> Types.type_defs -> Path.t -> Target.target -> Ident.t -> Types.type_defs
+val type_defs_new_ident_type: Ast.l -> Types.type_defs -> Path.t -> Target.non_ident_target -> Ident.t -> Types.type_defs
 
 
 (** {2 Constructing, checking and destructing expressions} *)
 (** An empty collection of entities *)
 val empty_used_entities : used_entities
 
-(** [get_checked_module_entities t_opt ml] gets all the modules, types, constants ... used by modules [ml] for target 
-  [t_opt]. If [t_opt] is [None], all targets are considered. *)
-val get_checked_modules_entities : Target.target option -> checked_module list -> used_entities
+(** [get_checked_module_entities targ ml] gets all the modules, types, constants ... used by modules [ml] for target 
+    [targ]. Notice that the identity backend won't throw parts of modules away. Therefore the result for the identiy backend
+    is the union of the results for all other backends. *)
+val get_checked_modules_entities : Target.target -> checked_module list -> used_entities
 
 
 (** {2 Miscellaneous} *)