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.

8 files changed, 89 insertions, 64 deletions

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 *)