Replacing "cast surgery" in LetIn by a proper field (see PR #404).

This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.

There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
  standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
  explicitly asked so.

See discussion at PR #417 for more information.

32 files changed, 280 insertions, 221 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e705e4e5a..e787e48bf 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -15,6 +15,7 @@ open Bigint
 open Decl_kinds
 open Extend
 open Libnames
+open Constrexpr_ops
 
 let unlock loc =
   let start, stop = Loc.unloc loc in
@@ -228,9 +229,10 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
   Element ("decl_notation", ["name", s], [pp_expr ce])
 and pp_local_binder lb = (* don't know what it is for now *)
   match lb with
-  | CLocalDef ((_, nam), ce) ->
+  | CLocalDef ((loc, nam), ce, ty) ->
       let attrs = ["name", string_of_name nam] in
-      pp_expr ~attr:attrs ce
+      let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in
+      pp_expr ~attr:attrs value
   | CLocalAssum (namll, _, ce) ->
       let ppl =
         List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
@@ -465,7 +467,8 @@ and pp_expr ?(attr=[]) e =
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
   | CRecord (_, _) -> assert false
-  | CLetIn (loc, (varloc, var), value, body) ->
+  | CLetIn (loc, (varloc, var), value, typ, body) ->
+      let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in
       xmlApply loc
         (xmlOperator "let" loc ::
          [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index ee6acde6b..53c97f6b6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -40,7 +40,7 @@ let names_of_local_assums bl =
   List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_)->[l]|CLocalPattern _ -> assert false) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -113,9 +113,10 @@ let rec constr_expr_eq e1 e2 =
   | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
       List.equal binder_expr_eq bl1 bl2 &&
       constr_expr_eq a1 a2
-  | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) ->
+  | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) ->
       Name.equal na1 na2 &&
       constr_expr_eq a1 a2 &&
+      Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
   | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) ->
       Option.equal Int.equal proj1 proj2 &&
@@ -212,8 +213,8 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
 | _ -> false
 
 and local_binder_eq l1 l2 = match l1, l2 with
-| CLocalDef (n1, e1), CLocalDef (n2, e2) ->
-  eq_located Name.equal n1 n2 && constr_expr_eq e1 e2
+| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
+  eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
   (** Don't care about the [binder_kind] *)
   List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
@@ -234,7 +235,7 @@ let constr_loc = function
   | CCoFix (loc,_,_) -> loc
   | CProdN (loc,_,_) -> loc
   | CLambdaN (loc,_,_) -> loc
-  | CLetIn (loc,_,_,_) -> loc
+  | CLetIn (loc,_,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
   | CRecord (loc,_) -> loc
@@ -270,7 +271,8 @@ let raw_cases_pattern_expr_loc = function
 
 let local_binder_loc = function
   | CLocalAssum ((loc,_)::_,_,t)
-  | CLocalDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
+  | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)
+  | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t))
   | CLocalAssum ([],_,_) -> assert false
   | CLocalPattern (loc,_,_) -> loc
 
@@ -285,7 +287,7 @@ let mkIdentC id  = CRef (Ident (Loc.ghost, id),None)
 let mkRefC r     = CRef (r,None)
 let mkCastC (a,k)  = CCast (Loc.ghost,a,k)
 let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b)
-let mkLetInC (id,a,b)   = CLetIn (Loc.ghost,id,a,b)
+let mkLetInC (id,a,t,b)   = CLetIn (Loc.ghost,id,a,t,b)
 let mkProdC (idl,bk,a,b)   = CProdN (Loc.ghost,[idl,bk,a],b)
 
 let mkAppC (f,l) =
@@ -308,7 +310,7 @@ let expand_pattern_binders mkC bl c =
     | b :: bl ->
         let (env, bl, c) = loop bl c in
         match b with
-        | CLocalDef (n, _) ->
+        | CLocalDef (n, _, _) ->
             let env = add_name_in_env env n in
             (env, b :: bl, c)
         | CLocalAssum (nl, _, _) ->
@@ -340,8 +342,8 @@ let mkCProdN loc bll c =
     match bll with
     | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
         CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | CLocalDef ((loc1,_) as id,b) :: bll ->
-        CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+    | CLocalDef ((loc1,_) as id,b,t) :: bll ->
+        CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c)
     | [] -> c
     | CLocalAssum ([],_,_) :: bll -> loop loc bll c
     | CLocalPattern (loc,p,ty) :: bll -> assert false
@@ -354,8 +356,8 @@ let mkCLambdaN loc bll c =
     match bll with
     | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
         CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | CLocalDef ((loc1,_) as id,b) :: bll ->
-        CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+    | CLocalDef ((loc1,_) as id,b,t) :: bll ->
+        CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c)
     | [] -> c
     | CLocalAssum ([],_,_) :: bll -> loop loc bll c
     | CLocalPattern (loc,p,ty) :: bll -> assert false
@@ -365,7 +367,7 @@ let mkCLambdaN loc bll c =
 
 let rec abstract_constr_expr c = function
   | [] -> c
-  | CLocalDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,abstract_constr_expr c bl)
   | CLocalAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
       (abstract_constr_expr c bl)
@@ -373,7 +375,7 @@ let rec abstract_constr_expr c = function
 
 let rec prod_constr_expr c = function
   | [] -> c
-  | CLocalDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,prod_constr_expr c bl)
   | CLocalAssum (idl,bk,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
       (prod_constr_expr c bl)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 9f200edef..45e3a19bc 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -46,7 +46,7 @@ val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
 val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
 val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr
+val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
 val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e723acd13..925e9517c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -601,8 +601,9 @@ let extern_optimal_prim_token scopes r r' =
 (* mapping decl                                                       *)
 
 let extended_glob_local_binder_of_decl loc = function
-  | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,t)
   | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t)
+  | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None)
+  | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t)
 
 (**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
@@ -699,8 +700,9 @@ let rec extern inctx scopes vars r =
 	   explicitize loc inctx [] (None,sub_extern false scopes vars f)
              (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
 
-  | GLetIn (loc,na,t,c) ->
-      CLetIn (loc,(loc,na),sub_extern false scopes vars t,
+  | GLetIn (loc,na,b,t,c) ->
+      CLetIn (loc,(loc,na),sub_extern false scopes vars b,
+              Option.map (extern_typ scopes vars) t,
               extern inctx scopes (add_vname vars na) c)
 
   | GProd (loc,na,bk,t,c) ->
@@ -828,7 +830,8 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
-       CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l)
+       CLocalDef((Loc.ghost,na), extern false scopes vars bd,
+                   Option.map (extern false scopes vars) ty) :: l)
 
   | GLocalAssum (_,na,bk,ty)::l ->
       let ty = extern_typ scopes vars ty in
@@ -1020,8 +1023,9 @@ let rec glob_of_pat env sigma = function
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
-  | PLetIn (na,t,c) ->
-      GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
+  | PLetIn (na,b,t,c) ->
+      GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
+              glob_of_pat (na::env) sigma c)
   | PLambda (na,t,c) ->
       GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
   | PIf (c,b1,b2) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 779959154..8fe6ce85e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -457,7 +457,10 @@ let intern_local_pattern intern lvar env p =
 
 let glob_local_binder_of_extended = function
   | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
-  | GLocalDef (loc,na,bk,c,t) -> (na,bk,Some c,t)
+  | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t)
+  | GLocalDef (loc,na,bk,c,None) ->
+      let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+      (na,bk,Some c,t)
   | GLocalPattern (loc,_,_,_,_) ->
       Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
 
@@ -468,14 +471,10 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let env, bl' = intern_assumption intern lvar env nal bk ty in
       let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in
       env, bl' @ bl
-  | CLocalDef((loc,na as locna),def) ->
-     let indef = intern env def in
-     let term, ty =
-       match indef with
-       | GCast (loc, b, Misctypes.CastConv t) -> b, t
-       | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)
-     in
-      (push_name_env lvar (impls_term_list indef) env locna,
+  | CLocalDef((loc,na as locna),def,ty) ->
+     let term = intern env def in
+     let ty = Option.map (intern env) ty in
+      (push_name_env lvar (impls_term_list term) env locna,
        GLocalDef (loc,na,Explicit,term,ty) :: bl)
   | CLocalPattern (loc,p,ty) ->
       let tyc =
@@ -566,15 +565,15 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
     (renaming',env), Name id'
 
 type letin_param =
-  | LPLetIn of Loc.t * (Name.t * glob_constr)
+  | LPLetIn of Loc.t * (Name.t * glob_constr * glob_constr option)
   | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t
 
 let make_letins =
   List.fold_right
     (fun a c ->
      match a with
-     | LPLetIn (loc,(na,b)) ->
-         GLetIn(loc,na,b,c)
+     | LPLetIn (loc,(na,b,t)) ->
+         GLetIn(loc,na,b,t,c)
      | LPCases (loc,(cp,il),id) ->
          let tt = (GVar(loc,id),(Name id,None)) in
          GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
@@ -582,8 +581,8 @@ let make_letins =
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
-  | GLocalDef (loc,na,_,b,_)::l ->
-      subordinate_letins (LPLetIn (loc,(na,b))::letins) l
+  | GLocalDef (loc,na,_,b,t)::l ->
+      subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l
   | GLocalAssum (loc,na,bk,t)::l ->
       let letins',rest = subordinate_letins [] l in
       letins',((loc,(na,bk,t)),letins)::rest
@@ -1600,9 +1599,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         intern env c2
     | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
 	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
-    | CLetIn (loc,na,c1,c2) ->
+    | CLetIn (loc,na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
-	GLetIn (loc, snd na, inc1,
+	let int = Option.map (intern_type env) t in
+	GLetIn (loc, snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index ececce340..7f11c0a3b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -109,10 +109,11 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
-    | ((CLocalDef (n, c)) :: tl) ->
+    | ((CLocalDef (n, c, t)) :: tl) ->
 	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
+	let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in
+	  aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl
 
     | CLocalPattern _ :: tl -> assert false
     | [] -> bdvars, l
@@ -131,10 +132,15 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
 	  else (id, loc) :: vs
 	else vs
     | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
+    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
 	let vs' = vars bound vs ty in
 	let bound' = add_name_to_ids bound na in
 	vars bound' vs' c
+    | GLetIn (loc,na,b,ty,c) ->
+	let vs' = vars bound vs b in
+	let vs'' = Option.fold_left (vars bound) vs' ty in
+	let bound' = add_name_to_ids bound na in
+	vars bound' vs'' c
     | GCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bound vs rtntypopt in
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
@@ -318,7 +324,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
             | _ -> ()
             in []
       | GLambda (loc, na, bk, t, b) -> abs na bk b
-      | GLetIn (loc, na, t, b) -> aux i b
+      | GLetIn (loc, na, b, t, c) -> aux i c
       | GRec (_, fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8900e2fab..59625426f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -36,7 +36,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
       on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GHole _, GHole _ -> true
   | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
-  | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
+  | GLetIn (_,na1,b1,t1,c1), GLetIn (_,na2,b2,t2,c2) when Name.equal na1 na2 ->
       on_true_do (f b1 b2 && f c1 c2) add na1
   | (GCases _ | GRec _
     | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
@@ -63,8 +63,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
   Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
   (eq_notation_constr vars) u1 u2
-| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
-  Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
+| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
+  Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
 | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
   let eqpat (p1, t1) (p2, t2) =
     List.equal cases_pattern_eq p1 p2 &&
@@ -168,8 +169,8 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c)
   | NProd (na,ty,c) ->
       let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c)
-  | NLetIn (na,b,c) ->
-      let e',na = g e na in GLetIn (loc,na,f e b,f e' c)
+  | NLetIn (na,b,t,c) ->
+      let e',na = g e na in GLetIn (loc,na,f e b,Option.map (f e) t,f e' c)
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -347,7 +348,7 @@ let notation_constr_and_vars_of_glob_constr a =
   | GApp (_,g,args) -> NApp (aux g, List.map aux args)
   | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
   | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
-  | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c)
+  | GLetIn (_,na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t,aux c)
   | GCases (_,sty,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
       NCases (sty,Option.map aux rtntypopt,
@@ -496,11 +497,12 @@ let rec subst_notation_constr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  NBinderList (id1,id2,r1',r2')
 
-  | NLetIn (n,r1,r2) ->
-      let r1' = subst_notation_constr subst bound r1
-      and r2' = subst_notation_constr subst bound r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  NLetIn (n,r1',r2')
+  | NLetIn (n,r1,t,r2) ->
+      let r1' = subst_notation_constr subst bound r1 in
+      let t' = Option.smartmap (subst_notation_constr subst bound) t in
+      let r2' = subst_notation_constr subst bound r2 in
+	if r1' == r1 && t == t' && r2' == r2 then raw else
+	  NLetIn (n,r1',t',r2')
 
   | NCases (sty,rtntypopt,rl,branches) ->
       let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
@@ -780,6 +782,11 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
+    let unify_opt_term alp v v' =
+      match v, v' with
+      | Some t, Some t' -> Some (unify_term alp t t')
+      | (Some _ as x), None | None, (Some _ as x) -> x
+      | None, None -> None in
     let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
     let unify_binder alp b b' =
       match b, b' with
@@ -788,7 +795,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
          alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t')
       | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') ->
          let alp, na = unify_name alp na na' in
-         alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_term alp t t')
+         alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
       | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') ->
          let alp, p = unify_pat alp p p' in
          alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
@@ -892,9 +899,9 @@ let rec match_iterated_binders islambda decls = function
       match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
   | GProd (loc,(Name _ as na),bk,t,b) when not islambda ->
       match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
-  | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
+  | GLetIn (loc,na,c,t,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	(GLocalDef (loc,na,Explicit (*?*), c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
+	(GLocalDef (loc,na,Explicit (*?*), c,t)::decls) b
   | b -> (decls,b)
 
 let remove_sigma x (terms,onlybinders,termlists,binderlists) =
@@ -1034,8 +1041,12 @@ let rec match_ inner u alp metas sigma a1 a2 =
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
   | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) ->
-     match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+  | GLetIn (_,na1,b1,_,c1), NLetIn (na2,b2,None,c2)
+  | GLetIn (_,na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
+     match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
+  | GLetIn (_,na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
+     match_binders u alp metas na1 na2
+       (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
   | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
       when sty1 == sty2
 	 && Int.equal (List.length tml1) (List.length tml2)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 178c1c1f9..d863e0561 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -28,7 +28,7 @@ let global_of_extended_global_head = function
         | NRef ref -> ref
         | NApp (rc, _) -> head_of rc
         | NCast (rc, _) -> head_of rc
-        | NLetIn (_, _, rc) -> head_of rc
+        | NLetIn (_, _, _, rc) -> head_of rc
         | _ -> raise Not_found in
       head_of syn_def
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 241204fe9..89e04b69d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -93,8 +93,8 @@ let rec fold_local_binders g f n acc b = function
       let nal = snd (List.split nal) in
       let n' = List.fold_right (name_fold g) nal n in
       f n (fold_local_binders g f n' acc b l) t
-  | CLocalDef ((_,na),t)::l ->
-      f n (fold_local_binders g f (name_fold g na n) acc b l) t
+  | CLocalDef ((_,na),c,t)::l ->
+      Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
   | CLocalPattern (_,pat,t)::l ->
       let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
       Option.fold_left (f n) acc t
@@ -105,7 +105,8 @@ let fold_constr_expr_with_binders g f n acc = function
   | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l
   | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
-  | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
+  | CLetIn (_,na,a,t,b) ->
+     f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
   | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
   | CCast (loc,a,CastCoerce) -> f n acc a
   | CNotation (_,_,(l,ll,bll)) ->
@@ -198,8 +199,8 @@ let map_local_binders f g e bl =
   let h (e,bl) = function
       CLocalAssum(nal,k,ty) ->
         (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
-    | CLocalDef((loc,na),ty) ->
-        (name_fold g na e, CLocalDef((loc,na),f e ty)::bl)
+    | CLocalDef((loc,na),c,ty) ->
+        (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
     | CLocalPattern (loc,pat,t) ->
         let ids = ids_of_pattern pat in
         (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in
@@ -214,7 +215,8 @@ let map_constr_expr_with_binders g f e = function
       let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
   | CLambdaN (loc,bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
-  | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
+  | CLetIn (loc,na,a,t,b) ->
+      CLetIn (loc,na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
   | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c)
   | CNotation (loc,n,(l,ll,bll)) ->
       (* This is an approximation because we don't know what binds what *)
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index d1b5697d7..49bafadc8 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -72,7 +72,7 @@ and constr_expr =
   | CCoFix of Loc.t * Id.t located * cofix_expr list
   | CProdN of Loc.t * binder_expr list * constr_expr
   | CLambdaN of Loc.t * binder_expr list * constr_expr
-  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr
+  | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr
   | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list
   | CApp of Loc.t * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
@@ -124,7 +124,7 @@ and recursion_order_expr =
 (** Anonymous defs allowed ?? *)
 and local_binder_expr =
   | CLocalAssum of Name.t located list * binder_kind * constr_expr
-  | CLocalDef of Name.t located * constr_expr
+  | CLocalDef of Name.t located * constr_expr * constr_expr option
   | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option
 
 and constr_notation_substitution =
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ce862cf8a..ced5a8b44 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -42,7 +42,7 @@ type glob_constr =
   | GApp of Loc.t * glob_constr * glob_constr list
   | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
   | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
-  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr
+  | GLetIn of Loc.t * Name.t * glob_constr * glob_constr option * glob_constr
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
   | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
@@ -80,7 +80,7 @@ and cases_clauses = cases_clause list
 
 type extended_glob_local_binder =
   | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr
-  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr
+  | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option
   | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr
 
 (** A globalised term together with a closure representing the value
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 1ab9980a5..753fa657a 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -30,7 +30,7 @@ type notation_constr =
   | NLambda of Name.t * notation_constr * notation_constr
   | NProd of Name.t * notation_constr * notation_constr
   | NBinderList of Id.t * Id.t * notation_constr * notation_constr
-  | NLetIn of Name.t * notation_constr * notation_constr
+  | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
   | NCases of case_style * notation_constr option *
       (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
       (cases_pattern list * notation_constr) list
diff --git a/intf/pattern.mli b/intf/pattern.mli
index 329ae837e..a32e7e4b9 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -68,7 +68,7 @@ type constr_pattern =
   | PProj of projection * constr_pattern
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
-  | PLetIn of Name.t * constr_pattern * constr_pattern
+  | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
   | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 592e16c6d..744d58b78 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -240,17 +240,15 @@ GEXTEND Gram
           mkCLambdaN (!@loc) bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 =
-	    Loc.merge (local_binders_loc bl) (constr_loc c1)
-	  in
-          CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+          CLetIn(!@loc,id,mkCLambdaN (constr_loc c1) bl c1,
+                 Option.map (mkCProdN (fst ty) bl) (snd ty), c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
           let (li,id) = match fixp with
               CFix(_,id,_) -> id
             | CCoFix(_,id,_) -> id
             | _ -> assert false in
-          CLetIn(!@loc,(li,Name id),fixp,c)
+          CLetIn(!@loc,(li,Name id),fixp,None,c)
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
 	  po = return_type;
 	  ":="; c1 = operconstr LEVEL "200"; "in";
@@ -466,9 +464,11 @@ GEXTEND Gram
       | "("; id=name; ":"; c=lconstr; ")" ->
           [CLocalAssum ([id],Default Explicit,c)]
       | "("; id=name; ":="; c=lconstr; ")" ->
-          [CLocalDef (id,c)]
+          (match c with
+          | CCast(_,c, CastConv t) -> [CLocalDef (id,c,Some t)]
+          | _ -> [CLocalDef (id,c,None)])
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [CLocalDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))]
+          [CLocalDef (id,c,Some t)]
       | "{"; id=name; "}" ->
           [CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 2b63ed6d6..3b233d6ef 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob =
 	 GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)
 
 let let_in_one_alias (id,pat) glob =
-  GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob)
+  GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob)
 
 let rec bind_primary_aliases map pat =
   match pat with
@@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
     let rids=ref ([],pat_vars) in
     let npatt= deanonymize rids patt in
       List.rev (fst !rids),npatt in
-  let term2 =
-    GLetIn(Loc.ghost,Anonymous,
-	   GCast(Loc.ghost,glob_of_pat npatt,
-		 CastConv app_ind),term1) in
+  let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 2426dd91c..084de31c0 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -42,7 +42,7 @@ let compose_glob_context =
     match bt with
       | Lambda n -> mkGLambda(n,t,acc)
       | Prod n -> mkGProd(n,t,acc)
-      | LetIn n -> mkGLetIn(n,t,acc)
+      | LetIn n -> mkGLetIn(n,t,None,acc)
   in
   List.fold_right compose_binder
 
@@ -489,7 +489,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		    | u::l -> 
 			match t with 
 			  | GLambda(loc,na,_,nat,b) -> 
-			      GLetIn(Loc.ghost,na,u,aux b l)
+			      GLetIn(Loc.ghost,na,u,None,aux b l)
 			  | _ -> 
 			      GApp(Loc.ghost,t,l)
 		in
@@ -535,7 +535,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		      args_res.result
 		}
 	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
-       	    | GLetIn(_,n,t,b) ->
+	    | GLetIn(_,n,v,t,b) ->
 		(* if we have [(let x := v in b) t1 ... tn] ,
 		   we discard our work and compute the list of constructor for
 		   [let x = v in (b t1 ... tn)] up to alpha conversion
@@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		  env
 		  funnames
 		  avoid
-		  (mkGLetIn(new_n,t,mkGApp(new_b,args)))
+		  (mkGLetIn(new_n,v,t,mkGApp(new_b,args)))
 	    | GCases _  | GIf _ | GLetTuple _ ->
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and
@@ -603,12 +603,13 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let new_env = raw_push_named (n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_prod n) t_res b_res
-    | GLetIn(_,n,v,b) ->
+    | GLetIn(loc,n,v,typ,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the value [t]
 	   and combine the two result
 	*)
+        let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
@@ -1115,8 +1116,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
-    | GLetIn(_,n,t,b) ->
+    | GLetIn(loc,n,v,t,b) ->
 	begin
+          let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
@@ -1131,7 +1133,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-	    | _ -> GLetIn(Loc.ghost,n,t,new_b),
+	    | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *)
 		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
@@ -1189,9 +1191,13 @@ let rec compute_cst_params relnames params = function
       compute_cst_params_from_app [] (params,rtl)
   | GApp(_,f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) ->
+  | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) ->
       let t_params = compute_cst_params relnames params t in
       compute_cst_params relnames t_params b
+  | GLetIn(_,_,v,t,b) ->
+      let v_params = compute_cst_params relnames params v in
+      let t_params = Option.fold_left (compute_cst_params relnames) v_params t in
+      compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
 		 discrimination ones *)
@@ -1202,12 +1208,12 @@ let rec compute_cst_params relnames params = function
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl'
-	when Id.compare id id' == 0 && not is_defined ->
+    | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl'
+	when Id.compare id id' == 0 ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
-let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts =
+let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts =
   let rels_params =
     Array.mapi
       (fun i args ->
@@ -1222,11 +1228,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
   let _ =
     try
       List.iteri
-	(fun i ((n,nt,is_defined) as param) ->
+	(fun i ((n,nt,typ) as param) ->
 	   if Array.for_all
 	     (fun l ->
-		let (n',nt',is_defined') = List.nth l i in
-		Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined')
+		let (n',nt',typ') = List.nth l i in
+		Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ')
 	     rels_params
 	   then
 	     l := param::!l
@@ -1241,15 +1247,15 @@ let rec rebuild_return_type rt =
   match rt with
     | Constrexpr.CProdN(loc,n,t') ->
 	Constrexpr.CProdN(loc,n,rebuild_return_type t')
-    | Constrexpr.CLetIn(loc,na,t,t') ->
-	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
+    | Constrexpr.CLetIn(loc,na,v,t,t') ->
+	Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t')
     | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
 				       Constrexpr.Default Decl_kinds.Explicit,rt],
 			    Constrexpr.CSort(Loc.ghost,GType []))
 
 
 let do_build_inductive
-      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list)
+      evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
       returned_types
       (rtl:glob_constr list) =
   let _time1 = System.get_time () in
@@ -1288,16 +1294,17 @@ let do_build_inductive
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
     let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
-      let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
+      let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
 	funargs
       in
       List.fold_right
-	(fun (n,t,is_defined) acc ->
-	   if is_defined
-	   then
+	(fun (n,t,typ) acc ->
+          match typ with
+          | Some typ ->
 	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
-	   else
+	  | None ->
 	     Constrexpr.CProdN
 	       (Loc.ghost,
 		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
@@ -1355,16 +1362,17 @@ let do_build_inductive
     rel_constructors
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
-    let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
+    let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list  =
       (snd (List.chop nrel_params funargs))
     in
     List.fold_right
-      (fun (n,t,is_defined) acc ->
-	 if is_defined
-	 then
+      (fun (n,t,typ) acc ->
+         match typ with
+         | Some typ ->
 	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+                              Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
-	 else
+	 | None ->
 	   Constrexpr.CProdN
 	   (Loc.ghost,
 	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
@@ -1391,11 +1399,12 @@ let do_build_inductive
   in
   let rel_params =
     List.map
-      (fun (n,t,is_defined) ->
-	 if is_defined
-	 then
-	   Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
-	 else
+      (fun (n,t,typ) ->
+         match typ with
+         | Some typ ->
+	   Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t,
+                                  Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
+	 | None ->
 	 Constrexpr.CLocalAssum
 	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 5bb1376e2..0cab5a6d3 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -12,7 +12,7 @@ val build_inductive :
  *)
   Evd.evar_map ->
   Term.pconstant list -> 
-  (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
+  (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
   unit
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 4e561fc7e..99f50437b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -15,7 +15,7 @@ let mkGVar id = GVar(Loc.ghost,id)
 let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
 let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
 let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b)
-let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b)
+let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c)
 let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl)
 let mkGSort s = GSort(Loc.ghost,s)
 let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
@@ -37,8 +37,8 @@ let glob_decompose_prod_or_letin =
   let rec glob_decompose_prod args = function
   | GProd(_,n,k,t,b) ->
       glob_decompose_prod ((n,None,Some t)::args) b
-  | GLetIn(_,n,t,b) ->
-      glob_decompose_prod ((n,Some t,None)::args) b
+  | GLetIn(_,n,b,t,c) ->
+      glob_decompose_prod ((n,Some b,t)::args) c
   | rt -> args,rt
   in
   glob_decompose_prod []
@@ -51,7 +51,7 @@ let glob_compose_prod_or_letin =
       fun concl decl ->
 	match decl with
 	  | (n,None,Some t) -> mkGProd(n,t,concl)
-	  | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl)
+	  | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl)
 	  | _ -> assert false)
 
 let glob_decompose_prod_n n =
@@ -73,8 +73,8 @@ let glob_decompose_prod_or_letin_n n =
       match c with
 	| GProd(_,n,_,t,b) ->
 	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| GLetIn(_,n,t,b) ->
-	    glob_decompose_prod (i-1) ((n,Some t,None)::args) b
+	| GLetIn(_,n,b,t,c) ->
+	    glob_decompose_prod (i-1) ((n,Some b,t)::args) c
 	| rt -> args,rt
   in
   glob_decompose_prod n []
@@ -150,10 +150,11 @@ let change_vars =
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | GLetIn(loc,name,def,b) ->
+      | GLetIn(loc,name,def,typ,b) ->
 	  GLetIn(loc,
 		 name,
 		 change_vars mapping def,
+		 Option.map (change_vars mapping) typ,
 		 change_vars (remove_name_from_mapping mapping name) b
 		)
       | GLetTuple(loc,nal,(na,rto),b,e) ->
@@ -272,10 +273,11 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt excluded t in
 	let new_b = alpha_rt excluded b in
 	GProd(loc,Anonymous,k,new_t,new_b)
-    | GLetIn(loc,Anonymous,t,b) ->
-	let new_t = alpha_rt excluded t in
+    | GLetIn(loc,Anonymous,b,t,c) ->
 	let new_b = alpha_rt excluded b in
-	GLetIn(loc,Anonymous,new_t,new_b)
+	let new_t = Option.map (alpha_rt excluded) t in
+	let new_c = alpha_rt excluded c in
+	GLetIn(loc,Anonymous,new_b,new_t,new_c)
     | GLambda(loc,Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
@@ -302,19 +304,17 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
 	GProd(loc,Name new_id,k,new_t,new_b)
-    | GLetIn(loc,Name id,t,b) ->
+    | GLetIn(loc,Name id,b,t,c) ->
 	let new_id = Namegen.next_ident_away id excluded in
-	let t,b =
-	  if Id.equal new_id id
-	  then t,b
-	  else
-	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
-	    (t,replace b)
+	let c =
+	  if Id.equal new_id id then c
+	  else change_vars (Id.Map.add id new_id Id.Map.empty) c
 	in
 	let new_excluded = new_id::excluded in
-	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	GLetIn(loc,Name new_id,new_t,new_b)
+	let new_t = Option.map (alpha_rt new_excluded) t in
+	let new_c = alpha_rt new_excluded c in
+	GLetIn(loc,Name new_id,new_b,new_t,new_c)
 
 
     | GLetTuple(loc,nal,(na,rto),t,b) ->
@@ -388,13 +388,20 @@ let is_free_in id =
     | GEvar _ -> false
     | GPatVar _ -> false
     | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) ->
+    | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> not (Id.equal id' id)
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
+    | GLetIn(_,n,b,t,c) ->
+	let check_in_c =
+	  match n with
+	    | Name id' -> not (Id.equal id' id)
+	    | _ -> true
+	in
+	is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c)
     | GCases(_,_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
@@ -473,11 +480,12 @@ let replace_var_by_term x_id term =
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt
-      | GLetIn(loc,name,def,b) ->
+      | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+      | GLetIn(loc,name,def,typ,b) ->
 	  GLetIn(loc,
 		 name,
 		 replace_var_by_pattern def,
+		 Option.map (replace_var_by_pattern) typ,
 		 replace_var_by_pattern b
 		)
       | GLetTuple(_,nal,_,_,_)
@@ -589,7 +597,7 @@ let ids_of_glob_constr c =
           ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
       | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
       | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
-      | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
+      | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc
       | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
       | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc
       | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
@@ -633,9 +641,9 @@ let zeta_normalize =
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
-      | GLetIn(_,Name id,def,b) ->
+      | GLetIn(_,Name id,def,typ,b) ->
 	  zeta_normalize_term (replace_var_by_term id def b)
-      | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
+      | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b
       | GLetTuple(loc,nal,(na,rto),def,b) ->
 	  GLetTuple(loc,
 		    nal,
@@ -690,7 +698,7 @@ let expand_as =
       | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args)
       | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b)
       | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b)
-      | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b)
+      | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b)
       | GLetTuple(loc,nal,(na,po),v,b) ->
 	  GLetTuple(loc,nal,(na,Option.map (expand_as map) po),
 		    expand_as map v, expand_as map b)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 179e8fe8d..84359a36b 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr
 val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr
-val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr
+val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr
 val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
 val mkGSort : glob_sort -> glob_constr
 val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d99c3fa04..d394fe313 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -129,7 +129,7 @@ let functional_induction with_clean c princl pat =
 
 let rec abstract_glob_constr c = function
   | [] -> c
-  | Constrexpr.CLocalDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl)
+  | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl)
   | Constrexpr.CLocalAssum (idl,k,t)::bl ->
       List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
         (abstract_glob_constr c bl)
@@ -192,8 +192,10 @@ let is_rec names =
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b)  ->
+    | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) ->
 	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
+    | GLetIn(_,na,b,t,c) ->
+	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
     | GLetTuple(_,nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
@@ -572,8 +574,8 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
 	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.CLocalDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') ->
-	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat)::aux),assoc)
+	  | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') ->
+	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
@@ -726,8 +728,8 @@ let rec add_args id new_args b =
       CLambdaN(loc,
 	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
 	       add_args id new_args  b1)
-  | CLetIn(loc,na,b1,b2) ->
-      CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
+  | CLetIn(loc,na,b1,t,b2) ->
+      CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
   | CAppExpl(loc,(pf,r,us),exprl) ->
       begin
 	match r with
@@ -865,7 +867,7 @@ let make_graph (f_ref:global_reference) =
 			  List.flatten
 			    (List.map
 			       (function
-				  | Constrexpr.CLocalDef (na,_)-> []
+				  | Constrexpr.CLocalDef (na,_,_)-> []
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb16..aed0fa331 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -70,8 +70,8 @@ let chop_rlambda_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
-	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
+	  | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
 	  | _ ->
 	      raise (CErrors.UserError(Some "chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e5c756f56..2aabfa003 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -34,7 +34,7 @@ val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
 val chop_rlambda_n : int -> Glob_term.glob_constr ->
-  (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr
 
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 7d7c3ad35..9c23be68a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -510,14 +510,14 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
         let args = filter_shift_stable lnk (arr1 @ arr2) in
         GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
     | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
-    | GLetIn(_,nme,bdy,trm) , _ ->
+    | GLetIn(_,nme,bdy,typ,trm) , _ ->
         let _ = prstr "\nICI2!\n" in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _, GLetIn(_,nme,bdy,trm) ->
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+    | _, GLetIn(_,nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3!\n" in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
@@ -528,14 +528,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
         let args = filter_shift_stable lnk (arr1 @ arr2) in
         GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
           (* FIXME: what if the function appears in the body of the let? *)
-    | GLetIn(_,nme,bdy,trm) , _ ->
+    | GLetIn(_,nme,bdy,typ,trm) , _ ->
       let _ = prstr "\nICI2 '!\n" in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
-    | _, GLetIn(_,nme,bdy,trm) ->
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+    | _, GLetIn(_,nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3 '!\n" in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,newtrm)
+        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
 
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 03c4ae47d..4d5594633 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -156,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None)
 let mkCLambda loc name ty t = 
    CLambdaN (loc, [[loc, name], Default Explicit, ty], t)
 let mkCLetIn loc name bo t = 
-   CLetIn (loc, (loc, name), bo, t)
+   CLetIn (loc, (loc, name), bo, None, t)
 let mkCCast loc t ty = CCast (loc,t, dC ty)
 (** Constructors for rawconstr *)
 let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None)
@@ -1193,7 +1193,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn loc x (a,(g,c)) = match c with
   | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b))
-  | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in
+  | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in
   match red with
   | T t -> let sigma, t = interp_term ist gl t in sigma, T t
   | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5ec44a68d..1cae8d16d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -264,7 +264,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
-      | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
+      | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) ->
+	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2
+
+      | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) ->
 	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cad5551c1..5a296de84 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -331,7 +331,7 @@ let extract_nondep_branches test c b l =
     match r,l with
       | r, [] -> r
       | GLambda (_,_,_,_,t), false::l -> strip l t
-      | GLetIn (_,_,_,t), true::l -> strip l t
+      | GLetIn (_,_,_,_,t), true::l -> strip l t
       (* FIXME: do we need adjustment? *)
       | _,_ -> assert false in
   if test c l then Some (strip l b) else None
@@ -341,7 +341,7 @@ let it_destRLambda_or_LetIn_names l c =
     match 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
+      | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c
       | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c
       | _, false::l ->
           (* eta-expansion *)
@@ -690,9 +690,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
       let c = detype (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
       let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
-      let c = if s != InProp then c else
-          GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in
-      GLetIn (dl, na', c, r)
+      let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in
+      GLetIn (dl, na', c, t, r)
 
 let detype_rel_context ?(lax=false) where avoid env sigma sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
@@ -764,9 +763,9 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
     | GProd (loc,id,k,t,c) ->
         let id = convert_name cl id in
         GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
-    | GLetIn (loc,id,b,e) ->
+    | GLetIn (loc,id,b,t,e) ->
         let id = convert_name cl id in
-        GLetIn(loc,id,detype_closed_glob cl b, detype_closed_glob cl e)
+        GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
     | GLetTuple (loc,ids,(n,r),b,e) ->
         let ids = List.map (convert_name cl) ids in
         let n = convert_name cl n in
@@ -825,10 +824,12 @@ let rec subst_glob_constr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  GProd (loc,n,bk,r1',r2')
 
-  | GLetIn (loc,n,r1,r2) ->
-      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  GLetIn (loc,n,r1',r2')
+  | GLetIn (loc,n,r1,t,r2) ->
+      let r1' = subst_glob_constr subst r1 in
+      let t' = Option.smartmap (subst_glob_constr subst) t in
+      let r2' = subst_glob_constr subst r2 in
+	if r1' == r1 && t == t' && r2' == r2 then raw else
+	  GLetIn (loc,n,r1',t',r2')
 
   | GCases (loc,sty,rtno,rl,branches) ->
       let rtno' = Option.smartmap (subst_glob_constr subst) rtno
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 51660818f..ebbfa195f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -77,8 +77,8 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) ->
   Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
   glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) ->
-  Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2
+| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) ->
+  Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2
 | GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) ->
   case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 &&
   List.equal tomatch_tuple_eq tp1 tp2 &&
@@ -152,10 +152,11 @@ let map_glob_constr_left_to_right f = function
       let comp1 = f ty in
       let comp2 = f c in
       GProd (loc,na,bk,comp1,comp2)
-  | GLetIn (loc,na,b,c) ->
+  | GLetIn (loc,na,b,t,c) ->
       let comp1 = f b in
+      let compt = Option.map f t in
       let comp2 = f c in
-      GLetIn (loc,na,comp1,comp2)
+      GLetIn (loc,na,comp1,compt,comp2)
   | GCases (loc,sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in
       let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
@@ -189,8 +190,10 @@ let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
 let fold_glob_constr f acc = function
   | GVar _ -> acc
   | GApp (_,c,args) -> List.fold_left f (f acc c) args
-  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) ->
+  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) ->
     f (f acc b) c
+  | GLetIn (_,_,b,t,c) ->
+    f (Option.fold_left f (f acc b) t) c
   | GCases (_,_,rtntypopt,tml,pl) ->
     let fold_pattern acc (_,idl,p,c) = f acc c in
     List.fold_left fold_pattern
@@ -225,8 +228,8 @@ let occur_glob_constr id =
       (occur ty) || (not (same_id na id) && (occur c))
     | GProd (loc,na,bk,ty,c) ->
       (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (loc,na,b,c) ->
-      (occur b) || (not (same_id na id) && (occur c))
+    | GLetIn (loc,na,b,t,c) ->
+      (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
     | GCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         || (List.exists (fun (tm,_) -> occur tm) tml)
@@ -270,10 +273,15 @@ let free_glob_vars =
   let rec vars bounded vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
     | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
+    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
 	let vs' = vars bounded vs ty in
 	let bounded' = add_name_to_ids bounded na in
        vars bounded' vs' c
+    | GLetIn (loc,na,b,ty,c) ->
+	let vs' = vars bounded vs b in
+	let vs'' = Option.fold_left (vars bounded) vs' ty in
+	let bounded' = add_name_to_ids bounded na in
+       vars bounded' vs'' c
     | GCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
@@ -346,7 +354,7 @@ let add_and_check_ident id set =
 
 let bound_glob_vars =
   let rec vars bound = function
-    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c ->
+    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
         let bound = name_fold add_and_check_ident na bound in
         fold_glob_constr vars bound c
     | GCases (loc,sty,rtntypopt,tml,pl) ->
@@ -460,7 +468,7 @@ let loc_of_glob_constr = function
   | GApp (loc,_,_) -> loc
   | GLambda (loc,_,_,_,_) -> loc
   | GProd (loc,_,_,_,_) -> loc
-  | GLetIn (loc,_,_,_) -> loc
+  | GLetIn (loc,_,_,_,_) -> loc
   | GCases (loc,_,_,_,_) -> loc
   | GLetTuple (loc,_,_,_,_) -> loc
   | GIf (loc,_,_,_,_) -> loc
@@ -512,9 +520,9 @@ let rec rename_glob_vars l = function
   | GLambda (loc,na,bk,t,c) ->
       let na',l' = update_subst na l in
       GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
-  | GLetIn (loc,na,b,c) ->
+  | GLetIn (loc,na,b,t,c) ->
       let na',l' = update_subst na l in
-      GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c)
+      GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
   (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
   | GCases (loc,ci,po,tomatchl,cls) ->
       let test_pred_pat (na,ino) =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 977d3dae1..79765a493 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -44,8 +44,9 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PProd (v1, t1, b1), PProd (v2, t2, b2) ->
   Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
-| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
-  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
+  Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
+  Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
 | PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
@@ -85,7 +86,8 @@ let rec occur_meta_pattern = function
   | PProj (_,arg) -> occur_meta_pattern arg
   | PLambda (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
   | PProd (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
-  | PLetIn (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
+  | PLetIn (na,b,t,c)  ->
+     Option.fold_left (fun b t -> b || occur_meta_pattern t) (occur_meta_pattern b) t || (occur_meta_pattern c)
   | PIf (c,c1,c2)  ->
       (occur_meta_pattern c) ||
       (occur_meta_pattern c1) || (occur_meta_pattern c2)
@@ -101,7 +103,7 @@ exception BoundPattern;;
 let rec head_pattern_bound t =
   match t with
     | PProd (_,_,b)  -> head_pattern_bound b
-    | PLetIn (_,_,b) -> head_pattern_bound b
+    | PLetIn (_,_,_,b) -> head_pattern_bound b
     | PApp (c,args)  -> head_pattern_bound c
     | PIf (c,_,_)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
@@ -132,7 +134,7 @@ let pattern_of_constr env sigma t =
     | Sort (Prop Pos) -> PSort GSet
     | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr env c
-    | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,
+    | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
 				  pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr env c,
 				pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
@@ -189,7 +191,7 @@ let map_pattern_with_binders g f l = function
   | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
   | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
   | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
-  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
+  | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
   | PCase (ci,po,p,pl) ->
     PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
@@ -274,11 +276,12 @@ let rec subst_pattern subst pat =
       let c2' = subst_pattern subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PProd (name,c1',c2')
-  | PLetIn (name,c1,c2) ->
+  | PLetIn (name,c1,t,c2) ->
       let c1' = subst_pattern subst c1 in
+      let t' = Option.smartmap (subst_pattern subst) t in
       let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PLetIn (name,c1',c2')
+	if c1' == c1 && t' == t && c2' == c2 then pat else
+	  PLetIn (name,c1',t',c2')
   | PSort _
   | PMeta _ -> pat
   | PIf (c,c1,c2) ->
@@ -343,9 +346,10 @@ let rec pat_of_raw metas vars = function
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | GLetIn (_,na,c1,c2) ->
+  | GLetIn (_,na,c1,t,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
+               Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
   | GSort (_,s) ->
       PSort s
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f92110ea5..15a48a6a3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -810,14 +810,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         iraise (e, info) in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-  | GLetIn(loc,name,c1,c2)      ->
-    let j =
-      match c1 with
-      | GCast (loc, c, CastConv t) ->
-	let tj = pretype_type empty_valcon env evdref lvar t in
-	  pretype (mk_tycon tj.utj_val) env evdref lvar c
-      | _ -> pretype empty_tycon env evdref lvar c1
-    in
+  | GLetIn(loc,name,c1,t,c2)      ->
+    let tycon1 =
+      match t with
+      | Some t ->
+	 mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val
+      | None ->
+         empty_tycon in
+    let j = pretype tycon1 env evdref lvar c1 in
     let t = evd_comb1 (Evarsolve.refresh_universes
       ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
       evdref j.uj_type in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d895693cc..0013d49a1 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -317,7 +317,7 @@ let tag_var = tag Tag.variable
             pr_sep_com spc (pr ltop) rhs))
 
   let begin_of_binder = function
-  CLocalDef((loc,_),_) -> fst (Loc.unloc loc)
+    | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc)
     | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
     | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc)
     | _ -> assert false
@@ -362,12 +362,9 @@ let tag_var = tag Tag.variable
   let pr_binder_among_many pr_c = function
     | CLocalAssum (nal,k,t) ->
       pr_binder true pr_c (nal,k,t)
-    | CLocalDef (na,c) ->
-      let c,topt = match c with
-        | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t
-        | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
-      surround (pr_lname na ++ pr_opt_type pr_c topt ++
-                  str":=" ++ cut() ++ pr_c c)
+    | CLocalDef (na,c,topt) ->
+      surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++
+                pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt)
     | CLocalPattern (loc,p,tyo) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
@@ -468,7 +465,7 @@ let tag_var = tag Tag.variable
           | CStructRec ->
             let names_of_binder = function
               | CLocalAssum (nal,_,_) -> nal
-              | CLocalDef (_,_) -> []
+              | CLocalDef (_,_,_) -> []
               | CLocalPattern _ -> assert false
             in let ids = List.flatten (List.map names_of_binder bl) in
                if List.length ids > 1 then
@@ -588,7 +585,7 @@ let tag_var = tag Tag.variable
               pr_fun_sep ++ pr spc ltop a),
           llambda
         )
-      | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
+      | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b)
           when Id.equal x x' ->
         return (
           hv 0 (
@@ -598,11 +595,12 @@ let tag_var = tag Tag.variable
               pr spc ltop b),
           lletin
         )
-      | CLetIn (_,x,a,b) ->
+      | CLetIn (_,x,a,t,b) ->
         return (
           hv 0 (
             hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :="
                    ++ pr spc ltop a ++ spc ()
+                   ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t
                    ++ keyword "in") ++
               pr spc ltop b),
           lletin
diff --git a/vernac/command.ml b/vernac/command.ml
index cdc1c88e6..8244ee534 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -55,7 +55,7 @@ let rec under_binders env sigma f n c =
 
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
-  | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
+  | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c)
   | CHole (loc, k, _, _) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
@@ -416,7 +416,7 @@ let rec check_anonymous_type ind =
     match ind with
     | GSort (_, GType []) -> true
     | GProd (_, _, _, _, e) 
-    | GLetIn (_, _, _, e)
+    | GLetIn (_, _, _, _, e)
     | GLambda (_, _, _, _, e)
     | GApp (_, e, _)
     | GCast (_, e, _) -> check_anonymous_type e
@@ -560,7 +560,7 @@ let check_named (loc, na) = match na with
 
 
 let check_param = function
-| CLocalDef (na, _) -> check_named na
+| CLocalDef (na, _, _) -> check_named na
 | CLocalAssum (nas, Default _, _) -> List.iter check_named nas
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
diff --git a/vernac/record.ml b/vernac/record.ml
index a6c8f8b36..51d89f155 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -108,7 +108,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       | _ -> ()
     in
       List.iter 
-	(function CLocalDef (b, _) -> error default_binder_kind b
+	(function CLocalDef (b, _, _) -> error default_binder_kind b
 	   | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
            | CLocalPattern (loc,_,_) ->
               Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps