Merge branch 'trunk' into pr379

13 files changed, 231 insertions, 228 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 59c24900d..53c97f6b6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -37,10 +37,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with
 let default_binder_kind = Default Explicit
 
 let names_of_local_assums bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> 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,9 +213,9 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
 | _ -> false
 
 and local_binder_eq l1 l2 = match l1, l2 with
-| LocalRawDef (n1, e1), LocalRawDef (n2, e2) ->
-  eq_located Name.equal n1 n2 && constr_expr_eq e1 e2
-| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, 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
 | _ -> false
@@ -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
@@ -269,10 +270,11 @@ let raw_cases_pattern_expr_loc = function
   | RCPatOr (loc,_) -> loc
 
 let local_binder_loc = function
-  | LocalRawAssum ((loc,_)::_,_,t)
-  | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
-  | LocalRawAssum ([],_,_) -> assert false
-  | LocalPattern (loc,_,_) -> loc
+  | CLocalAssum ((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
 
 let local_binders_loc bll = match bll with
   | [] -> Loc.ghost
@@ -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,17 +310,17 @@ let expand_pattern_binders mkC bl c =
     | b :: bl ->
         let (env, bl, c) = loop bl c in
         match b with
-        | LocalRawDef (n, _) ->
+        | CLocalDef (n, _, _) ->
             let env = add_name_in_env env n in
             (env, b :: bl, c)
-        | LocalRawAssum (nl, _, _) ->
+        | CLocalAssum (nl, _, _) ->
             let env = List.fold_left add_name_in_env env nl in
             (env, b :: bl, c)
-        | LocalPattern (loc, p, ty) ->
+        | CLocalPattern (loc, p, ty) ->
             let ni = Hook.get fresh_var env c in
             let id = (loc, Name ni) in
             let b =
-              LocalRawAssum
+              CLocalAssum
                 ([id], Default Explicit,
                  match ty with
                  | Some ty -> ty
@@ -338,13 +340,13 @@ let expand_pattern_binders mkC bl c =
 let mkCProdN loc bll c =
   let rec loop loc bll c =
     match bll with
-    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+    | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
         CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | LocalRawDef ((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
-    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalPattern (loc,p,ty) :: bll -> assert false
+    | CLocalAssum ([],_,_) :: bll -> loop loc bll c
+    | CLocalPattern (loc,p,ty) :: bll -> assert false
   in
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
@@ -352,32 +354,32 @@ let mkCProdN loc bll c =
 let mkCLambdaN loc bll c =
   let rec loop loc bll c =
     match bll with
-    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+    | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
         CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | LocalRawDef ((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
-    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalPattern (loc,p,ty) :: bll -> assert false
+    | CLocalAssum ([],_,_) :: bll -> loop loc bll c
+    | CLocalPattern (loc,p,ty) :: bll -> assert false
   in
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
 
 let rec abstract_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::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)
-  | LocalPattern _::_ -> assert false
+  | CLocalPattern _::_ -> assert false
 
 let rec prod_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::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)
-  | LocalPattern _::_ -> assert false
+  | CLocalPattern _::_ -> assert false
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index a92da035f..45e3a19bc 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -23,8 +23,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
 (** Equality on [constr_expr]. This is a syntactical one, which is oblivious to
     some parsing details, including locations. *)
 
-val local_binder_eq : local_binder -> local_binder -> bool
-(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
+val local_binder_eq : local_binder_expr -> local_binder_expr -> bool
+(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *)
 
 val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
 (** Equality on [binding_kind] *)
@@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
 val constr_loc : constr_expr -> Loc.t
 val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
 val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
-val local_binders_loc : local_binder list -> Loc.t
+val local_binders_loc : local_binder_expr list -> Loc.t
 
 (** {6 Constructors}*)
 
@@ -46,22 +46,22 @@ 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 list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
 
-val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [abstract_constr_expr], with location *)
 
-val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
 val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
 val expand_pattern_binders :
-  (Loc.t -> local_binder list -> constr_expr -> constr_expr) ->
-  local_binder list -> constr_expr -> local_binder list * constr_expr
+  (Loc.t -> local_binder_expr list -> constr_expr -> constr_expr) ->
+  local_binder_expr list -> constr_expr -> local_binder_expr list * constr_expr
 
 (** {6 Destructors}*)
 
@@ -78,9 +78,9 @@ val coerce_to_name : constr_expr -> Name.t located
 
 val default_binder_kind : binder_kind
 
-val names_of_local_binders : local_binder list -> Name.t located list
+val names_of_local_binders : local_binder_expr list -> Name.t located list
 (** Retrieve a list of binding names from a list of binders. *)
 
-val names_of_local_assums : local_binder list -> Name.t located list
-(** Same as [names_of_local_binders], but does not take the [let] bindings into
+val names_of_local_assums : local_binder_expr list -> Name.t located list
+(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
     account. *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8debc06bb..f272d219a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -598,6 +598,14 @@ let extern_optimal_prim_token scopes r r' =
   | _ -> raise No_match
 
 (**********************************************************************)
+(* mapping decl                                                       *)
+
+let extended_glob_local_binder_of_decl loc = function
+  | (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                                    *)
 
 let extern_glob_sort = function
@@ -692,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) ->
@@ -756,7 +765,7 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
-                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in
+                 let bl = List.map (extended_glob_local_binder_of_decl loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -773,7 +782,7 @@ let rec extern inctx scopes vars r =
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
-                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in
+                 let bl = List.map (extended_glob_local_binder_of_decl loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -817,33 +826,32 @@ and factorize_lambda inctx scopes vars na bk aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
-  | (Inl na,bk,Some bd,ty)::l ->
+  | GLocalDef (_,na,bk,bd,ty)::l ->
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
-       LocalRawDef((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)
 
-  | (Inl na,bk,None,ty)::l ->
+  | GLocalAssum (_,na,bk,ty)::l ->
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
-          (assums,ids,LocalRawAssum(nal,k,ty')::l)
+          (assums,ids,CLocalAssum(nal,k,ty')::l)
             when constr_expr_eq ty ty' &&
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
-               LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l)
+               CLocalAssum((Loc.ghost,na)::nal,k,ty')::l)
         | (assums,ids,l) ->
             (na::assums,na::ids,
-             LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
-
-  | (Inr p,bk,Some bd,ty)::l -> assert false
+             CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l))
 
-  | (Inr p,bk,None,ty)::l ->
+  | GLocalPattern (_,(p,_),_,bk,ty)::l ->
       let ty =
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l)
+      (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
@@ -1017,8 +1025,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) ->
@@ -1056,5 +1065,5 @@ let extern_rel_context where env sigma sign =
   let where = Option.map EConstr.of_constr where in
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
-  let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
+  let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index f617faa38..b39339450 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -41,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  Context.Rel.t -> local_binder list
+  Context.Rel.t -> local_binder_expr list
 
 (** Printing options *)
 val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8fee191af..d75487ecf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -65,8 +65,6 @@ type var_internalization_data =
 type internalization_env =
     (var_internalization_data) Id.Map.t
 
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
-
 type ltac_sign = {
   ltac_vars : Id.Set.t;
   ltac_bound : Id.Set.t;
@@ -306,12 +304,12 @@ let reset_tmp_scope env = {env with tmp_scope = None}
 
 let rec it_mkGProd loc2 env body =
   match env with
-      (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
     | [] -> body
 
 let rec it_mkGLambda loc2 env body =
   match env with
-      (loc1, (na, bk, _, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -399,7 +397,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
     env fvs in
   let bl = List.map
     (fun (id, loc) ->
-      (loc, (Name id, b, None, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+      (loc, (Name id, b, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -414,7 +412,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-  in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',None,ty')) :: List.rev bl
+  in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl
 
 let intern_assumption intern lvar env nal bk ty =
   let intern_type env = intern (set_type_scope env) in
@@ -426,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty =
       List.fold_left
 	(fun (env, bl) (loc, na as locna) ->
           (push_name_env lvar impls env locna,
-           (loc,(na,k,None,locate_if_hole loc na ty))::bl))
+           (loc,(na,k,locate_if_hole loc na ty))::bl))
 	(env, []) nal
   | Generalized (b,b',t) ->
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
@@ -457,47 +455,47 @@ let intern_local_pattern intern lvar env p =
        env)
     env (free_vars_of_pat [] p)
 
-type binder_data =
-  | BDRawDef of (Loc.t * glob_binder)
-  | BDPattern of
-      (Loc.t * (cases_pattern * Id.t list) *
-         (bool ref *
-          (Notation_term.tmp_scope_name option *
-           Notation_term.tmp_scope_name list)
-          option ref * Notation_term.notation_var_internalization_type)
-         Names.Id.Map.t *
-       intern_env * constr_expr)
+let glob_local_binder_of_extended = function
+  | GLocalAssum (loc,na,bk,t) -> (na,bk,None,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.")
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
 
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
-  | LocalRawAssum(nal,bk,ty) ->
+  | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
-      let bl' = List.map (fun a -> BDRawDef a) bl' in
+      let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in
       env, bl' @ bl
-  | LocalRawDef((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,
-       (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl)
-  | LocalPattern (loc,p,ty) ->
+  | 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 =
         match ty with
         | Some ty -> ty
         | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
+      let il = List.map snd (free_vars_of_pat [] p) in
       let cp =
         match !intern_cases_pattern_fwd (None,env.scopes) p with
         | (_, [(_, cp)]) -> cp
         | _ -> assert false
       in
-      let il = List.map snd (free_vars_of_pat [] p) in
-      (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl)
+      let ienv = Id.Set.elements env.ids in
+      let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+      let na = (loc, Name id) in
+      let bk = Default Explicit in
+      let _, bl' = intern_assumption intern lvar env [na] bk tyc in
+      let _,(_,bk,t) = List.hd bl' in
+      (env, GLocalPattern(loc,(cp,il),id,bk,t) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -567,35 +565,29 @@ 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)]))
 
-let rec subordinate_letins intern letins = function
+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 *)
-  | BDRawDef (loc,(na,_,Some b,t))::l ->
-      subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l
-  | BDRawDef (loc,(na,bk,None,t))::l ->
-      let letins',rest = subordinate_letins intern [] l in
+  | 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
-  | BDPattern (loc,u,lvar,env,tyc) :: l ->
-      let ienv = Id.Set.elements env.ids in
-      let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
-      let na = (loc, Name id) in
-      let bk = Default Explicit in
-      let _, bl' = intern_assumption intern lvar env [na] bk tyc in
-      let bl' = List.map (fun a -> BDRawDef a) bl' in
-      subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l)
+  | GLocalPattern (loc,u,id,bk,t) :: l ->
+      subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l)
   | [] ->
       letins,[]
 
@@ -609,10 +601,11 @@ let terms_of_binders bl =
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
   let rec extract_variables = function
-    | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l
-    | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l
-    | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term."
-    | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l
+    | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l
+    | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
+    | GLocalDef (loc,Anonymous,_,_,_)::l
+    | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term."
+    | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l
     | [] -> [] in
   extract_variables bl
 
@@ -674,7 +667,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (bl,(scopt,subscopes)) = Id.Map.find x binders in
 	let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
-	let letins,bl = subordinate_letins intern [] bl in
+	let letins,bl = subordinate_letins [] bl in
         let termin = aux (terms,None,None) (renaming,env) terminator in
 	let res = List.fold_left (fun t binder ->
 	    aux (terms,Some(y,binder),Some t) subinfos iter)
@@ -1545,10 +1538,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	     let intern_ro_arg f =
 	       let before, after = split_at_annot bl n in
 	       let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
-               let rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in
 	       let ro = f (intern env') in
-	       let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in
-               let rbefore = List.map (fun a -> BDRawDef a) rbefore in
+	       let n' = Option.map (fun _ -> List.count (function GLocalAssum _ -> true | _ -> false (* remove let-ins *)) rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, (env',rbl) =
@@ -1560,24 +1551,19 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       | CMeasureRec (m,r) ->
 		   intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
 	     in
-	     let bl =
-               List.rev_map
-                 (function
-                  | BDRawDef a -> a
-                  | BDPattern (loc,_,_,_,_) ->
-                      Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")) rbl in
-	       ((n, ro), bl, intern_type env' ty, env')) dl in
+	     let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
+             ((n, ro), bl, intern_type env' ty, env')) dl in
         let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name -> 
 					     let (_,bli,tyi,_) = idl_temp.(i) in
-					     let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
+					     let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
 	GRec (loc,GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
-              Array.map (fun (_,bl,_,_) -> List.map snd bl) idl,
+              Array.map (fun (_,bl,_,_) -> bl) idl,
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
     | CCoFix (loc, (locid,iddef), dl) ->
@@ -1591,20 +1577,18 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let idl_tmp = Array.map
           (fun ((loc,id),bl,ty,_) ->
             let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
-            let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> 
-                      Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in
-            (List.rev rbl,
+            (List.rev (List.map glob_local_binder_of_extended rbl),
              intern_type env' ty,env')) dl in
 	let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
 	     let env'' = List.fold_left_i (fun i en name ->
 					     let (bli,tyi,_) = idl_tmp.(i) in
-					     let cofix_args =  List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
+					     let cofix_args =  List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
 	GRec (loc,GCoFix n,
               Array.of_list lf,
-              Array.map (fun (bl,_,_) -> List.map snd bl) idl,
+              Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
     | CProdN (loc,[],c2) ->
@@ -1615,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 ->
@@ -2070,18 +2055,11 @@ let intern_context global_level env impl_env binders =
   let lvar = (empty_ltac_sign, Id.Map.empty) in
   let lenv, bl = List.fold_left
 	    (fun (lenv, bl) b ->
-               let bl = List.map (fun a -> BDRawDef a) bl in
 	       let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
-               let bl =
-                 List.map
-                   (function
-                    | BDRawDef a -> a
-                    | BDPattern (loc,_,_,_,_) ->
-                        Loc.raise ~loc (Stream.Error "pattern with quote not allowed here")) bl in
 	       (env, bl))
 	    ({ids = extract_ids env; unb = false;
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
-  (lenv.impls, List.map snd bl)
+  (lenv.impls, List.map glob_local_binder_of_extended bl)
   with InternalizationError (loc,e) ->
     user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index ae7f511f4..758d4e650 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -75,8 +75,6 @@ type ltac_sign = {
 
 val empty_ltac_sign : ltac_sign
 
-type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr)
-
 (** {6 Internalization performs interpretation of global names and notations } *)
 
 val intern_constr : env -> constr_expr -> glob_constr
@@ -90,7 +88,7 @@ val intern_gen : typing_constraint -> env ->
 val intern_pattern : env -> cases_pattern_expr ->
   Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
+val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -159,16 +157,16 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
-  env -> evar_map ref -> local_binder list ->
+  env -> evar_map ref -> local_binder_expr list ->
   internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
 (*   ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
+(*   env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
   
 (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder list ->  *)
+(*   env -> evar_map -> local_binder_expr list ->  *)
 (*   internalization_env *  *)
 (*   ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 77a8ed680..7f11c0a3b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -102,19 +102,20 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
 let ids_of_names l =
   List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
 
-let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
+let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
   let rec aux bdvars l c = match c with
-      ((LocalRawAssum (n, _, c)) :: tl) ->
+      ((CLocalAssum (n, _, c)) :: tl) ->
 	let bound = ids_of_names 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
 
-    | ((LocalRawDef (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
 
-    | LocalPattern _ :: tl -> assert false
+    | CLocalPattern _ :: tl -> assert false
     | [] -> bdvars, l
   in aux bound l binders
 
@@ -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/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d0327e506..71009ec3c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -25,7 +25,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
   Id.t list -> Id.t list
 
 val free_vars_of_binders :
-  ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
+  ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurrence *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 549e8e787..8b4fadb5a 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,
@@ -497,11 +498,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
@@ -781,18 +783,23 @@ 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
-      | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
+      | GLocalAssum (loc,na,bk,t), GLocalAssum (_,na',bk',t') ->
          let alp, na = unify_name alp na na' in
-         alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
-      | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
+         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, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
-      | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
+         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, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+         alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
       | _ -> raise No_match in
     let rec unify alp bl bl' =
     match bl, bl' with
@@ -821,16 +828,16 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
       else raise No_match in
     let unify_term_binder c b' =
       match c, b' with
-      | GVar (_, id), (Inl na', bk', None, t') (* assum *) ->
-         (Inl (unify_id id na'), bk', None, t')
-      | c, (Inr p', bk', None, t') (* pattern *) ->
+      | GVar (loc, id), GLocalAssum (_, na', bk', t') ->
+         GLocalAssum (loc, unify_id id na', bk', t')
+      | c, GLocalPattern (loc, (p',ids), id, bk', t') ->
          let p = pat_binder_of_term c in
-         (Inr (unify_pat p p'), bk', None, t')
+         GLocalPattern (loc, (unify_pat p p',ids), id, bk', t')
       | _ -> raise No_match in
     let rec unify cl bl' =
     match cl, bl' with
     | [], [] -> []
-    | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl'
+    | c :: cl, GLocalDef (_, _, _, _, t) :: bl' -> unify cl bl'
     | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
     | _ -> raise No_match in
     let bl = unify cl bl' in
@@ -883,19 +890,19 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
 let glue_letin_with_decls = true
 
 let rec match_iterated_binders islambda decls = function
-  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+  | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
       when islambda && Id.equal p e ->
-      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
-  | GLambda (_,na,bk,t,b) when islambda ->
-      match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
-  | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+      match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
+  | GLambda (loc,na,bk,t,b) when islambda ->
+      match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
+  | GProd (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
       when not islambda && Id.equal p e ->
-      match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
-  | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
-      match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
-  | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
+      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,t,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	((Inl na,Explicit (*?*), Some 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) =
@@ -972,29 +979,29 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
 
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-  | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+  | GLambda (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
     NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
-      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders true [GLocalPattern(loc,(cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
-      let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
+  | GLambda (loc,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
+      let (decls,b) = match_iterated_binders true [GLocalAssum (loc,na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
   (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-  | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+  | GProd (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
     NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
-      let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders true [GLocalPattern (loc,(cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
-  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
+  | GProd (loc,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
       when na1 != Anonymous ->
-      let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
+      let (decls,b) = match_iterated_binders false [GLocalAssum (loc,na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
@@ -1003,18 +1010,18 @@ let rec match_ inner u alp metas sigma a1 a2 =
       match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+  | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
     NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [GLocalPattern (loc,(cp,ids),p,bk,t)] in
       match_in u alp metas sigma b1 b2
-  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
+  | GLambda (loc,na,bk,t,b1), NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in
       match_in u alp metas sigma b1 b2
-  | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
+  | GProd (loc,na,bk,t,b1), NProd (Name id,_,b2)
       when is_bindinglist_meta id metas && na != Anonymous ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in
       match_in u alp metas sigma b1 b2
 
   (* Matching compositionally *)
@@ -1035,8 +1042,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)
@@ -1102,7 +1113,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)]
+          bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
       match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c8fcbf741..a61ba172e 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -47,12 +47,9 @@ val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
 
 exception No_match
 
-type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
-      glob_constr option * glob_constr
 val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
-      (glob_decl2 list * subscopes) list
+      (extended_glob_local_binder list * subscopes) list
 
 val match_notation_constr_cases_pattern :
   cases_pattern -> interpretation ->
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 fd57b70ca..89e04b69d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -89,13 +89,13 @@ let rec fold_constr_expr_binders g f n acc b = function
       f n acc b
 
 let rec fold_local_binders g f n acc b = function
-  | LocalRawAssum (nal,bk,t)::l ->
+  | CLocalAssum (nal,bk,t)::l ->
       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
-  | LocalRawDef ((_,na),t)::l ->
-      f n (fold_local_binders g f (name_fold g na n) acc b l) t
-  | LocalPattern (_,pat,t)::l ->
+  | 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)) ->
@@ -160,7 +161,7 @@ let split_at_annot bl na =
       end
   | Some (loc, id) ->
       let rec aux acc = function
-	| LocalRawAssum (bls, k, t) as x :: rest ->
+	| CLocalAssum (bls, k, t) as x :: rest ->
             let test (_, na) = match na with
             | Name id' -> Id.equal id id'
             | Anonymous -> false
@@ -171,12 +172,12 @@ let split_at_annot bl na =
             | _ ->
               let ans = match l with
               | [] -> acc
-              | _ -> LocalRawAssum (l, k, t) :: acc
+              | _ -> CLocalAssum (l, k, t) :: acc
               in
-              (List.rev ans, LocalRawAssum (r, k, t) :: rest)
+              (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
-        | LocalPattern (loc,_,_) :: rest ->
+	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
+        | CLocalPattern (loc,_,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ~loc 
@@ -196,13 +197,13 @@ let map_binders f g e bl =
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let h (e,bl) = function
-      LocalRawAssum(nal,k,ty) ->
-        (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
-    | LocalRawDef((loc,na),ty) ->
-        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
-    | LocalPattern (loc,pat,t) ->
+      CLocalAssum(nal,k,ty) ->
+        (map_binder g e nal, CLocalAssum(nal,k,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, LocalPattern (loc,pat,Option.map (f e) t)::bl) in
+        (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
@@ -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/interp/topconstr.mli b/interp/topconstr.mli
index 95d702f8d..b6ac40041 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -25,7 +25,7 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool
 (** Specific function for interning "in indtype" syntax of "match" *)
 val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
 
-val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list
+val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
 
 (** Used in typeclasses *)