diff --git a/Changelog.md b/Changelog.md
index fe658c18c..dc5cc06fb 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,14 @@
 # Changelog
 
+## [2.0.2] - 22/01/2024
+
+Requires Elpi 1.18.1 and Coq 8.19.
+
+### API
+- Fix `coq.elaborate-*` does not erase the type annotation of `Let`s (regression
+  introduced in 2.0.1). This fix may introduce differences in generated names
+- Fix `coq.elaborate-*` are not affected anymore by printing options
+
 ## [2.0.1] - 29/12/2023
 
 Requires Elpi 1.18.1 and Coq 8.19.
diff --git a/apps/derive/tests/test_projK.v b/apps/derive/tests/test_projK.v
index b5eaea801..0369e608d 100644
--- a/apps/derive/tests/test_projK.v
+++ b/apps/derive/tests/test_projK.v
@@ -59,11 +59,11 @@ Check eq_refl 0 : projEnvelope1 nat 1 1 (Envelope nat 0 1) = 0.
 Check projEnvelope2 : forall A, A -> A -> zeta A -> A.
 Check eq_refl 0 : projEnvelope2 nat 1 1 (Envelope nat 1 0) = 0.
 Check projRedex1 : forall A, A -> beta A -> A.
-Check projWhy1 : forall n : peano, match n with 
+Check projWhy1 : forall n : peano, match n return Type with 
                     | Zero => peano
                     | Succ _ => unit
                     end -> iota -> peano.
-Check projWhy2 : forall n : peano, match n with 
+Check projWhy2 : forall n : peano, match n return Type with 
                     | Zero => peano
                     | Succ _ => unit
                     end -> iota -> { i : peano & match i with Zero => peano | Succ _ => unit end }.
diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml
index 5bf057cf8..c3921b18c 100644
--- a/src/coq_elpi_utils.ml
+++ b/src/coq_elpi_utils.ml
@@ -87,6 +87,9 @@ let safe_destApp sigma t =
 let mkGHole =
   DAst.make
     (Glob_term.(GHole GInternalHole))
+let mkGSort =
+  DAst.make
+    (Glob_term.(GSort (UAnonymous { rigid = UState.univ_flexible_alg })))
     
 let mkApp ~depth t l =
   match l with
@@ -229,17 +232,378 @@ let rec list_map_acc f acc = function
       let acc, xs = list_map_acc f acc xs in
       acc, x :: xs
 
+let rec dest_globLam g =
+  match DAst.get g with
+  | Glob_term.GLambda(name,_,_,bo) ->
+      let names, bo = dest_globLam bo in
+      name :: names, bo
+  | _ -> [], g
+  
+let is_unknown_constructor x = 
+  Names.GlobRef.ConstructRef x = Coqlib.lib_ref "elpi.unknown_constructor"
+
 let rec fix_detype x = match DAst.get x with
   | Glob_term.GEvar _ -> mkGHole
   | _ -> Glob_ops.map_glob_constr fix_detype x
+
+let detype_qvar sigma q =
+  let open Glob_term in
+  match UState.id_of_qvar (Evd.evar_universe_context sigma) q with
+  | Some id -> GLocalQVar (CAst.make (Names.Name.Name id))
+  | None -> GQVar q
+let detype_quality sigma q =
+  let open Glob_term in
+  let open Sorts.Quality in
+  match q with
+  | QConstant q -> GQConstant q
+  | QVar q -> GQualVar (detype_qvar sigma q)
+  
+let detype_level_name sigma l =
+  let open Glob_term in
+  if Univ.Level.is_set l then GSet else
+    match UState.id_of_level (Evd.evar_universe_context sigma) l with
+    | Some id -> GLocalUniv (CAst.make id)
+    | None -> GUniv l
+let detype_level sigma l =
+  let open Glob_term in
+  UNamed (detype_level_name sigma l)
+    
+let detype_universe sigma u =
+  List.map (Util.on_fst (detype_level_name sigma)) (Univ.Universe.repr u)
+  
+let detype_sort ku sigma x =
+  let open Sorts in
+  let open Glob_term in
+  match x with
+  | Prop -> UNamed (None, [GProp,0])
+  | SProp -> UNamed (None, [GSProp,0])
+  | Set -> UNamed (None, [GSet,0])
+  | Type u when ku -> UNamed (None, detype_universe sigma u)
+  | QSort (q, u) when ku -> UNamed (Some (detype_qvar sigma q), detype_universe sigma u)
+  | _ -> UAnonymous {rigid=UState.UnivRigid}
+(*
+let detype_relevance_info sigma na =
+  match Evarutil.nf_relevance sigma na with
+  | Relevant -> Some Glob_term.GRelevant
+  | Irrelevant -> Some Glob_term.GIrrelevant
+  | RelevanceVar q -> Some (Glob_term.GRelevanceVar (detype_qvar sigma q))
+*)
+
+let detype_instance ku sigma l =
+  if not ku then None
+  else
+    let open EConstr in
+    let l = EInstance.kind sigma l in
+    if UVars.Instance.is_empty l then None
+    else
+      let qs, us = UVars.Instance.to_array l in
+      let qs = List.map (detype_quality sigma) (Array.to_list qs) in
+      let us = List.map (detype_level sigma) (Array.to_list us) in
+      Some (qs, us)
+
+
+let it_destRLambda_or_LetIn_names l c =
+  let open Glob_term in
+  let rec aux l nal c =
+    match DAst.get c, l with
+      | _, [] -> (List.rev nal,c)
+      | GLambda (na,_,_,c), false::l -> aux l (na::nal) c
+      | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c
+      | _ -> nYI "detype eta"
+  in aux l [] c
+      
+
+  (** Reimplementation of kernel case expansion functions in more lenient way *)
+module RobustExpand :
+sig
+val return_clause : Environ.env -> Evd.evar_map -> Names.Ind.t ->
+  EConstr.EInstance.t -> EConstr.t array -> EConstr.case_return -> EConstr.rel_context * EConstr.t
+val branch : Environ.env -> Evd.evar_map -> Names.Construct.t ->
+  EConstr.EInstance.t -> EConstr.t array -> EConstr.case_branch -> EConstr.rel_context * EConstr.t
+end =
+struct
+open Context.Rel.Declaration
+open Declarations
+open UVars
+open Constr
+open Vars
+
+let instantiate_context u subst nas ctx =
+  let rec instantiate i ctx = match ctx with
+  | [] -> []
+  | LocalAssum (_, ty) :: ctx ->
+    let ctx = instantiate (pred i) ctx in
+    let ty = substnl subst i (subst_instance_constr u ty) in
+    LocalAssum (nas.(i), ty) :: ctx
+  | LocalDef (_, ty, bdy) :: ctx ->
+    let ctx = instantiate (pred i) ctx in
+    let ty = substnl subst i (subst_instance_constr u ty) in
+    let bdy = substnl subst i (subst_instance_constr u bdy) in
+    LocalDef (nas.(i), ty, bdy) :: ctx
+  in
+  let () = if not (Int.equal (Array.length nas) (List.length ctx)) then raise_notrace Exit in
+  instantiate (Array.length nas - 1) ctx
+
+let return_clause env sigma ind u params ((nas, p),_) =
+  try
+    let u = EConstr.Unsafe.to_instance u in
+    let params = EConstr.Unsafe.to_constr_array params in
+    let () = if not @@ Environ.mem_mind (fst ind) env then raise_notrace Exit in
+    let mib = Environ.lookup_mind (fst ind) env in
+    let mip = mib.mind_packets.(snd ind) in
+    let paramdecl = subst_instance_context u mib.mind_params_ctxt in
+    let paramsubst = subst_of_rel_context_instance paramdecl params in
+    let realdecls, _ = CList.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+    let self =
+      let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
+      let inst = Instance.(abstract_instance (length u)) in
+      mkApp (mkIndU (ind, inst), args)
+    in
+    let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
+    let realdecls = instantiate_context u paramsubst nas realdecls in
+    List.map EConstr.of_rel_decl realdecls, p
+  with e when CErrors.noncritical e ->
+    let dummy na = LocalAssum (na, EConstr.mkProp) in
+    List.rev (CArray.map_to_list dummy nas), p
+
+let branch env sigma (ind, i) u params (nas, br) =
+  try
+    let u = EConstr.Unsafe.to_instance u in
+    let params = EConstr.Unsafe.to_constr_array params in
+    let () = if not @@ Environ.mem_mind (fst ind) env then raise_notrace Exit in
+    let mib = Environ.lookup_mind (fst ind) env in
+    let mip = mib.mind_packets.(snd ind) in
+    let paramdecl = subst_instance_context u mib.mind_params_ctxt in
+    let paramsubst = subst_of_rel_context_instance paramdecl params in
+    let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+    let ctx, _ = CList.chop mip.mind_consnrealdecls.(i - 1) ctx in
+    let ctx = instantiate_context u paramsubst nas ctx in
+    List.map EConstr.of_rel_decl ctx, br
+  with e when CErrors.noncritical e ->
+    let dummy na = LocalAssum (na, EConstr.mkProp) in
+    List.rev (CArray.map_to_list dummy nas), br
+
+end
+
 let detype ?(keepunivs=false) env sigma t =
-  (* To avoid turning named universes into unnamed ones *)
-  let options =
-    if keepunivs then Flags.with_option Constrextern.print_universes
-    else Flags.without_option Constrextern.print_universes in
-  let gbody =
-    options (Detyping.detype Detyping.Now Names.Id.Set.empty env sigma) t in
-  fix_detype gbody
+  let open Glob_term in
+  let open EConstr in
+  let open Context.Rel.Declaration in
+  debug Pp.(fun () -> str"detype: " ++ Printer.pr_econstr_env env sigma t);
+
+  let fresh (names,e) name ty =
+    let open Names.Name in
+    let mk_fresh was =
+      let id = Namegen.next_name_away was names in
+      Name id, (Names.Id.Set.add id names,e) in
+    match name with
+    | Anonymous ->
+        let noccurs sigma i = function
+          | None -> true
+          | Some t -> Vars.noccurn sigma i t in
+        let name, names = Namegen.compute_displayed_name_in_gen  noccurs e sigma names name ty in
+        name, (names, e)
+    | Name id when Names.Id.Set.mem id names -> mk_fresh name
+    | Name id as x -> x, (Names.Id.Set.add id names,e) in
+
+  let push_rel d env c =
+    let name = Context.Rel.Declaration.get_name d in
+    let name, (names, env) = fresh env name (Some c) in
+    (names, EConstr.push_rel (Context.Rel.Declaration.set_name name d) env), name in
+  let push_occurring_rel d env =
+    let name = Context.Rel.Declaration.get_name d in
+    let name, (names, env) = fresh env name None in
+    (names, EConstr.push_rel (Context.Rel.Declaration.set_name name d) env), name in
+  
+  let lookup_rel i (_,env) = Environ.lookup_rel i env in
+
+  let unknown_inductive = Coqlib.lib_ref "elpi.unknown_inductive" in
+  
+let rec detype_binder env name bo ty t =
+  let gty = aux env ty in
+  let gbo = Option.map (aux env) bo in
+  (*let rinfo = detype_relevance_info sigma binder_relevance in*)
+  let env, name = push_rel (LocalAssum(name,ty)) env t in
+  let gt = aux env t in
+  name, gbo, gty, gt
+
+and aux env t =
+    match kind sigma t with
+    | Rel i ->
+        begin match lookup_rel i env |> get_name  with
+        | Names.Name.Anonymous -> assert false
+        | Names.Name.Name x -> DAst.make @@ GVar x
+        | exception Not_found -> assert false
+        end
+    | Var x -> 
+        (* Discriminate between section variable and non-section variable *)
+        DAst.make 
+          (try let _ = Environ.lookup_named x (snd env) in GRef (Names.GlobRef.VarRef x, None)
+          with Not_found -> GVar x)
+    | Meta _ -> assert false
+    | Evar _ -> mkGHole
+    | Sort s -> DAst.make @@ GSort (detype_sort keepunivs sigma (ESorts.kind sigma s))
+    | Cast(t,k,ty) -> DAst.make @@ GCast(aux env t,Some k,aux env ty)
+    | Prod (name,ty,t) ->
+        let name, _, gty, gt = detype_binder env name None ty t in
+        DAst.make @@ GProd (name, Explicit, gty, gt)
+    | Lambda (name,ty,t) ->
+      let name, _, gty, gt = detype_binder env name None ty t in
+      DAst.make @@ GLambda (name, Explicit, gty, gt)
+    | LetIn (name,bo,ty,t) ->
+      let name, gbo, gty, gt = detype_binder env name (Some bo) ty t in
+      DAst.make @@ GLetIn (name, Option.get gbo, Some gty, gt)
+    | App(hd,args) ->
+      DAst.make @@ GApp(aux env  hd, CArray.map_to_list (aux env) args)
+    | Int i -> DAst.make @@ GInt i
+    | Float i -> DAst.make @@ GFloat i
+    | Array(u,a,d,ty) -> DAst.make @@ GArray(detype_instance keepunivs sigma u,CArray.map (aux env) a,aux env d, aux env ty)
+    | Const(c,u) -> DAst.make @@ GRef (Names.GlobRef.ConstRef c, detype_instance keepunivs sigma u)
+    | Ind(c,u) -> DAst.make @@ GRef (Names.GlobRef.IndRef c, detype_instance keepunivs sigma u)
+    | Construct(c,u) -> DAst.make @@ GRef (Names.GlobRef.ConstructRef c, detype_instance keepunivs sigma u)
+    | Proj(p,r,c) ->
+        if Names.Projection.unfolded p then
+          let open Names in
+          let c = aux env c in
+          let id = Label.to_id @@ Projection.label p in
+          let nargs, parg =
+            try
+              let _, mip = Global.lookup_inductive (Projection.inductive p) in
+              mip.mind_consnrealargs.(0), Projection.arg p
+            with e when !Flags.in_debugger ->
+              (* kinda weird printing but the name should be enough to
+                indicate which projection it is *)
+              1, 0
+          in
+          let pathole = DAst.make @@ PatVar Anonymous in
+          let patargs = List.init nargs (fun i ->
+              if Int.equal i parg
+              then DAst.make @@ PatVar (Name id)
+              else pathole)
+          in
+          let pat = DAst.make @@ PatCstr ((Projection.inductive p, 1), patargs, Anonymous) in
+          let br = ([id], [pat], DAst.make @@ GVar id) in
+          (* MatchStyle looks relatively heavy *)
+          DAst.make @@ GCases (LetPatternStyle, None, [c, (Anonymous, None)], [CAst.make br])
+        else
+          let pars = Names.Projection.npars p in
+          let hole = DAst.make @@ GHole (GInternalHole) in
+          let args = CList.make pars hole in
+          DAst.make @@ GApp (DAst.make @@ GRef (Names.GlobRef.ConstRef (Names.Projection.constant p), None),
+          (args @ [aux env c]))
+    | Fix((vn,_ as nvn),(names,tys,bodies)) ->
+      let env, names =
+        list_map_acc (fun env (n,ty) ->
+          push_occurring_rel (LocalAssum (n,ty)) env) env (CArray.combine names tys |> CArray.to_list) in 
+      let n = Array.length tys in
+      let v = CArray.map3
+        (fun c t i -> share_names (i+1) [] env c (Vars.lift n t))
+        bodies tys vn in
+      DAst.make @@ GRec(GFix (Array.map (fun i -> Some i) (fst nvn), snd nvn),CArray.map_of_list (function Names.Name.Name x -> x | _ -> assert false) names,
+         Array.map (fun (bl,_,_) -> bl) v,
+         Array.map (fun (_,_,ty) -> ty) v,
+         Array.map (fun (_,bd,_) -> bd) v)
+    | CoFix _ -> nYI "cofix"
+    | Case (ci,u,pms,p,iv,c,[|bl|]) when unknown_inductive = Names.GlobRef.IndRef ci.ci_ind ->
+        let tomatch = aux env c in
+        let map i br =
+          let (ctx, body) = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) u pms br in
+          EConstr.it_mkLambda_or_LetIn body ctx
+        in
+        let bl = map 0 bl in
+        let bl' = aux env bl in
+        let constagsl = ci.ci_pp_info.cstr_tags in
+        let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl' in
+  
+        DAst.make @@ GLetTuple (nal,( (*Anonymous,None*) (Name (Names.Id.of_string "xxx"),Some mkGHole)),tomatch,d)
+    | Case (ci,u,pms,p,iv,c,bl) ->
+      detype_case env (ci, u, pms, p, iv, c, bl)
+
+  and share_names n l env bo ty =
+    if n = 0 then
+      List.rev l, aux env bo, aux env ty
+    else
+      match EConstr.kind sigma bo, EConstr.kind sigma ty with
+      | LetIn (_,b,_,x), _ -> share_names n l env (Vars.subst1 b x) ty
+      | _, LetIn (_,b,_,x) -> share_names n l env bo (Vars.subst1 b x)
+      | Lambda (na,lty,bo), Prod (na',_,ty) ->
+          let na = Nameops.Name.pick_annot na na' in
+          let decl = LocalAssum (na,lty) in
+          let lty = aux env lty in
+          let env, na = push_rel decl env bo in
+          share_names (n-1) ((na,Explicit,None,lty)::l) env bo ty
+      | _, Prod (na,lty,ty) ->
+          let decl = LocalAssum (na,lty) in
+          let lty = aux env lty in
+          let env, na = push_occurring_rel decl env in
+          let bo = mkApp (Vars.lift 1 bo,[|mkRel 1|]) in
+          share_names (n-1) ((na,Explicit,None,lty)::l) env bo ty
+      | _ -> assert false
+
+  and detype_case env (ci, univs, params, p, iv, c, bl) =
+    let open Constr in
+    let tomatch = aux env c in
+    let tomatch =
+      let _, mip = Global.lookup_inductive ci.ci_ind in
+      let hole = DAst.make @@ GHole (GInternalHole) in
+      let indices = CList.make mip.mind_nrealargs hole in
+      let t = EConstr.mkApp (EConstr.mkIndU (ci.ci_ind,univs), params) in
+      DAst.make @@ GCast (tomatch, None, Glob_ops.mkGApp (aux env t) indices) in
+
+    let alias, aliastyp, pred =
+      let (ctx, p) = RobustExpand.return_clause (snd env) sigma ci.ci_ind univs params p in
+      let p = EConstr.it_mkLambda_or_LetIn p ctx in
+      let p = aux env p in
+      let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in
+      let n,typ = match DAst.get typ with
+        | GLambda (x,_,t,c) -> x, c
+        | _ -> Anonymous, typ in
+      let aliastyp =
+        if List.for_all (Names.Name.equal Anonymous) nl then None
+        else Some (CAst.make (ci.ci_ind,nl)) in
+      n, aliastyp, Some typ
+    in
+    let constructs = Array.init (Array.length bl) (fun i -> (ci.ci_ind,i+1)) in
+    let constagsl = ci.ci_pp_info.cstr_tags in
+    let eqnl = detype_eqns env constructs constagsl (ci, univs, params, bl) in
+    DAst.make @@ GCases (RegularStyle,pred,[tomatch,(alias,aliastyp)],eqnl)
+        
+  and detype_eqns env constructs consnargsl bl =
+    let (ci, u, pms, bl) = bl in
+    CArray.to_list
+      (CArray.map3 (detype_eqn env u pms) constructs consnargsl bl)
+
+  and detype_eqn env u pms constr construct_nargs br =
+    let ctx, body = RobustExpand.branch (snd env) sigma constr u pms br in
+    let branch = EConstr.it_mkLambda_or_LetIn body ctx in
+    let make_pat decl env b ids =
+      let env, na = push_rel decl env b in
+      let ids = match na with Names.Name.Name x -> Names.Id.Set.add x ids | _ -> ids in
+      DAst.make (PatVar na), env, ids
+    in
+    let rec buildrec ids patlist env n b =
+      if Int.equal n 0 then
+        CAst.make @@
+          (Names.Id.Set.elements ids,
+            [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)],
+            aux env b)
+      else match EConstr.kind sigma b with
+        | Lambda (x,t,b) ->
+              let pat,env,new_ids = make_pat (LocalAssum (x,t)) env b ids in
+              buildrec new_ids (pat::patlist) env (pred n) b
+  
+        | LetIn (x,b,t,b') ->
+              let pat,env,new_ids = make_pat (LocalDef (x,b,t)) env b' ids in
+              buildrec new_ids (pat::patlist) env (pred n) b'
+  
+        | _ -> assert false
+    in
+    buildrec Names.Id.Set.empty [] env (List.length ctx) branch in
+
+  let namesr = Environ.rel_context env |> Context.Rel.to_vars in
+  let namesv = Environ.named_context env |> Context.Named.to_vars in
+  let x = aux (Names.Id.Set.union namesr namesv, env) t in
+  x
 
 let detype_closed_glob env sigma closure =
   let gbody = Detyping.detype_closed_glob Names.Id.Set.empty env sigma closure in
diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v
index 1f31a7d17..cb5d73fba 100644
--- a/tests/test_API_elaborate.v
+++ b/tests/test_API_elaborate.v
@@ -186,3 +186,15 @@ Elpi Typecheck.
 
 Elpi detype #[universes(polymorphic)] Definition f@{u|Set < u} (x : Type@{u}) := x.
 
+Section Test.
+
+Variable C : Type.
+
+
+Elpi Query lp:{{
+
+  std.assert-ok! (coq.elaborate-skeleton {{ list C }} TY E) "that was easy 2"
+
+}}.
+
+End Test.
\ No newline at end of file
diff --git a/theories/elpi.v b/theories/elpi.v
index 3bff41c2f..9aeb4d6dc 100644
--- a/theories/elpi.v
+++ b/theories/elpi.v
@@ -19,6 +19,7 @@ Register hole as elpi.hole.
    in terms like "let (a,b...) := t in ..." *)
 Inductive unknown_inductive : Prop := unknown_constructor.
 Register unknown_inductive as elpi.unknown_inductive.
+Register unknown_constructor as elpi.unknown_constructor.
 
 (* Special global constant used to signal a datum of type gref which
    has no corresponding Coq global reference. This typically signals