merging conflicts with the original "trunk__CLEANUP__Context__2" branch

11 files changed, 186 insertions, 155 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index cddc55515..b29ceb78b 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -23,6 +23,7 @@ open Declarations
 open Mod_subst
 open Globnames
 open Printer
+open Context.Named.Declaration
 
 (** For a constant c in a module sealed by an interface (M:T and
     not M<:T), [Global.lookup_constant] may return a [constant_body]
@@ -145,7 +146,7 @@ let push (r : Context.Rel.Declaration.t) (ctx : Context.Rel.t) = r :: ctx
 
 let rec traverse current ctx accu t = match kind_of_term t with
 | Var id ->
-  let body () = match Global.lookup_named id with (_, body, _) -> body in
+  let body () = Global.lookup_named id |> get_value in
   traverse_object accu body (VarRef id)
 | Const (kn, _) ->
   let body () = Global.body_of_constant_body (lookup_constant kn) in
@@ -208,8 +209,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
   let (_, graph, ax2ty) = traverse (label_of gr) t in
   let fold obj _ accu = match obj with
   | VarRef id ->
-    let (_, body, t) = Global.lookup_named id in
-    if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
+    let decl = Global.lookup_named id in
+    if is_local_assum decl then ContextObjectMap.add (Variable id) t accu
     else accu
   | ConstRef kn ->
     let cb = lookup_constant kn in
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index c143243b1..3d053c2e1 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -25,6 +25,7 @@ open Tactics
 open Ind_tables
 open Misctypes
 open Proofview.Notations
+open Context.Rel.Declaration
 
 let out_punivs = Univ.out_punivs
 
@@ -146,17 +147,17 @@ let build_beq_scheme mode kn =
                              ) ext_rel_list in
 
         let eq_input = List.fold_left2
-          ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *)
+          ( fun a b decl -> (* mkLambda(n,b,a) ) *)
                 (* here I leave the Naming thingy so that the type of
                   the function is more readable for the user *)
-                mkNamedLambda (eqName n) b a )
+                mkNamedLambda (eqName (get_name decl)) b a )
                 c (List.rev eqs_typ) lnamesparrec
        in
-        List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *)
+        List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
           (* Same here , hoping the auto renaming will do something good ;)  *)
           mkNamedLambda
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl)  a) eq_input lnamesparrec
  in
  let make_one_eq cur =
   let u = Univ.Instance.empty in
@@ -248,7 +249,7 @@ let build_beq_scheme mode kn =
                     | 0 -> Lazy.force tt
                     | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
                       for ndx = 0 to nb_cstr_args-1 do
-                        let _,_,cc = List.nth constrsi.(i).cs_args ndx in
+                        let cc = get_type (List.nth constrsi.(i).cs_args ndx) in
                           let eqA, eff' = compute_A_equality rel_list
                                           nparrec
                                           (nparrec+3+2*nb_cstr_args)
@@ -267,14 +268,14 @@ let build_beq_scheme mode kn =
                           (Array.sub eqs 1 (nb_cstr_args - 1))
                   )
    		  in
-		    (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc
+		    (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc
                     (constrsj.(j).cs_args)
 		)
-	      else ar2.(j) <- (List.fold_left (fun a (p,q,r) ->
-			mkLambda (p,r,a)) (Lazy.force ff) (constrsj.(j).cs_args) )
+	      else ar2.(j) <- (List.fold_left (fun a decl ->
+			mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
 	    done;
 
-	  ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
+	  ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a))
 			(mkCase (ci,do_predicate rel_list nb_cstr_args,
 				  mkVar (Id.of_string "Y") ,ar2))
 			 (constrsi.(i).cs_args))
@@ -487,8 +488,8 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   create, from a list of ids [i1,i2,...,in] the list
   [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al  )]
 *)
-let list_id l = List.fold_left ( fun a (n,_,t) -> let s' =
-      match n with
+let list_id l = List.fold_left ( fun a decl -> let s' =
+      match get_name decl with
         Name s -> Id.to_string s
       | Anonymous -> "A" in
           (Id.of_string s',Id.of_string ("eq_"^s'),
@@ -535,9 +536,9 @@ let compute_bl_goal ind lnamesparrec nparrec =
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+      List.fold_left (fun a decl -> mkNamedProd
+                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl) a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -678,9 +679,9 @@ let compute_lb_goal ind lnamesparrec nparrec =
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
       ) lb_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+      List.fold_left (fun a decl -> mkNamedProd
+                (match (get_name decl) with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl)  a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -819,9 +820,9 @@ let compute_dec_goal ind lnamesparrec nparrec =
       let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
-      List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
-                t  a) eq_input lnamesparrec
+      List.fold_left (fun a decl -> mkNamedProd
+                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (get_type decl) a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 6bb047af0..2089bc944 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -21,6 +21,7 @@ open Globnames
 open Constrintern
 open Constrexpr
 open Sigma.Notations
+open Context.Rel.Declaration
 (*i*)
 
 open Decl_kinds
@@ -75,14 +76,14 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
 let type_ctx_instance evars env ctx inst subst =
   let rec aux (subst, instctx) l = function
-    (na, b, t) :: ctx ->
-      let t' = substl subst t in
+    decl :: ctx ->
+      let t' = substl subst (get_type decl) in
       let c', l =
-	match b with
-	| None -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
-	| Some b -> substl subst b, l
+	match decl with
+	| LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
+	| LocalDef (_,b,_) -> substl subst b, l
       in
-      let d = na, Some c', t' in
+      let d = get_name decl, Some c', t' in
 	aux (c' :: subst, d :: instctx) l ctx
     | [] -> subst
   in aux (subst, []) inst (List.rev ctx)
@@ -131,7 +132,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     match bk with
     | Implicit ->
 	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
-	  (fun avoid (clname, (id, _, t)) ->
+	  (fun avoid (clname, _) ->
 	    match clname with
 	    | Some (cl, b) ->
 		let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
@@ -154,10 +155,11 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
     let cl, u = Typeclasses.typeclass_univ_instance k in
     let _, args = 
-      List.fold_right (fun (na, b, t) (args, args') ->
-	match b with
-	| None -> (List.tl args, List.hd args :: args')
-	| Some b -> (args, substl args' b :: args'))
+      List.fold_right (fun decl (args, args') ->
+        let open Context.Rel.Declaration in
+	match decl with
+	| LocalAssum _ -> (List.tl args, List.hd args :: args')
+	| LocalDef (_,b,_) -> (args, substl args' b :: args'))
 	(snd cl.cl_context) (args, [])
     in
       cl, u, c', ctx', ctx, len, imps, args
@@ -180,7 +182,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     if abstract then
       begin
 	let subst = List.fold_left2
-	  (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+	  (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
 	  [] subst (snd k.cl_context)
 	in
 	let (_, ty_constr) = instance_constructor (k,u) subst in
@@ -224,10 +226,10 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    in
 	    let props, rest =
 	      List.fold_left
-		(fun (props, rest) (id,b,_) ->
-		  if Option.is_empty b then 
+		(fun (props, rest) decl ->
+		  if is_local_assum decl then
 		    try
-		      let is_id (id', _) = match id, get_id id' with
+		      let is_id (id', _) = match get_name decl, get_id id' with
 			| Name id, (_, id') -> Id.equal id id'
 			| Anonymous, _ -> false
                       in
@@ -261,7 +263,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    None, termtype
 	| Some (Inl subst) ->
 	  let subst = List.fold_left2
-	    (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+	    (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
 	    [] subst (k.cl_props @ snd k.cl_context)
 	  in
 	  let (app, ty_constr) = instance_constructor (k,u) subst in
@@ -344,9 +346,11 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 let named_of_rel_context l =
   let acc, ctx =
     List.fold_right
-      (fun (na, b, t) (subst, ctx) ->
-	let id = match na with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
-	let d = (id, Option.map (substl subst) b, substl subst t) in
+      (fun decl (subst, ctx) ->
+        let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+	let d = match decl with
+	  | LocalAssum (_,t) -> id, None, substl subst t
+	  | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
 	  (mkVar id :: subst, d :: ctx))
       l ([], [])
   in ctx
@@ -358,7 +362,7 @@ let context poly l =
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
   let fullctx = Context.Rel.map subst fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
-  let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
+  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx
     with e when Errors.noncritical e ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index aa5f7a692..166fe94ea 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -37,6 +37,7 @@ open Indschemes
 open Misctypes
 open Vernacexpr
 open Sigma.Notations
+open Context.Rel.Declaration
 
 let do_universe poly l = Declare.do_universe poly l
 let do_constraint poly l = Declare.do_constraint poly l
@@ -45,9 +46,9 @@ let rec under_binders env sigma f n c =
   if Int.equal n 0 then f env sigma c else
     match kind_of_term c with
       | Lambda (x,t,c) ->
-	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) sigma f (n-1) c)
+	  mkLambda (x,t,under_binders (push_rel (LocalAssum (x,t)) env) sigma f (n-1) c)
       | LetIn (x,b,t,c) ->
-	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) sigma f (n-1) c)
+	  mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
       | _ -> assert false
 
 let rec complete_conclusion a cs = function
@@ -264,6 +265,7 @@ let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
   List.rev refs, status
 
 let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
   let l = 
@@ -278,7 +280,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
   let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
     let (t,ctx),imps = interp_assumption evdref env ienv [] c in
     let env =
-      push_named_context (List.map (fun (_,id) -> (id,None,t)) idl) env in
+      push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun (_,id) ienv ->
       let impls = compute_internalization_data env Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
@@ -340,7 +342,7 @@ let do_assumptions kind nl l = match l with
 (* 3b| Mutual inductive definitions *)
 
 let push_types env idl tl =
-  List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env)
+  List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env)
     env idl tl
 
 type structured_one_inductive_expr = {
@@ -383,8 +385,8 @@ let mk_mltype_data evdref env assums arity indname =
   (is_ml_type,indname,assums)
 
 let prepare_param = function
-  | (na,None,t) -> out_name na, LocalAssum t
-  | (na,Some b,_) -> out_name na, LocalDef b
+  | LocalAssum (na,t) -> out_name na, Entries.LocalAssum t
+  | LocalDef (na,b,_) -> out_name na, Entries.LocalDef b
 
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
@@ -438,12 +440,12 @@ let interp_cstrs evdref env impls mldata arity ind =
 
 let sign_level env evd sign =
   fst (List.fold_right
-    (fun (_,b,t as d) (lev,env) ->
-      match b with
-      | Some _ -> (lev, push_rel d env)
-      | None ->
+    (fun d (lev,env) ->
+      match d with
+      | LocalDef _ -> lev, push_rel d env
+      | LocalAssum _ ->
 	let s = destSort (Reduction.whd_betadeltaiota env 
-			    (nf_evar evd (Retyping.get_type_of env evd t)))
+			    (nf_evar evd (Retyping.get_type_of env evd (get_type d))))
 	in
 	let u = univ_of_sort s in
 	  (Univ.sup u lev, push_rel d env))
@@ -454,7 +456,7 @@ let sup_list min = List.fold_left Univ.sup min
 let extract_level env evd min tys = 
   let sorts = List.map (fun ty -> 
     let ctx, concl = Reduction.dest_prod_assum env ty in
-      sign_level env evd ((Anonymous, None, concl) :: ctx)) tys 
+      sign_level env evd (LocalAssum (Anonymous, concl) :: ctx)) tys
   in sup_list min sorts
 
 let is_flexible_sort evd u =
@@ -560,8 +562,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let indnames = List.map (fun ind -> ind.ind_name) indl in
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
-  let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
-  let params = List.map (fun (na,_,_) -> out_name na) assums in
+  let assums = List.filter is_local_assum ctx_params in
+  let params = List.map (fun decl -> out_name (get_name decl)) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in
@@ -881,12 +883,13 @@ let lt_ref = make_qref "Init.Peano.lt"
 
 let rec telescope = function
   | [] -> assert false
-  | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
-  | (n, None, t) :: tl ->
+  | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1
+  | LocalAssum (n, t) :: tl ->
       let ty, tys, (k, constr) =
 	List.fold_left
-	  (fun (ty, tys, (k, constr)) (n, b, t) ->
-	    let pred = mkLambda (n, t, ty) in
+	  (fun (ty, tys, (k, constr)) decl ->
+            let t = get_type decl in
+            let pred = mkLambda (get_name decl, t, ty) in
 	    let ty = Universes.constr_of_global (Lazy.force sigT).typ in
 	    let intro = Universes.constr_of_global (Lazy.force sigT).intro in
 	    let sigty = mkApp (ty, [|t; pred|]) in
@@ -895,21 +898,21 @@ let rec telescope = function
 	  (t, [], (2, mkRel 1)) tl
       in
       let (last, subst) = List.fold_right2
-	(fun pred (n, b, t) (prev, subst) ->
+        (fun pred decl (prev, subst) ->
+          let t = get_type decl in
 	  let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
 	  let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
 	  let proj1 = applistc p1 [t; pred; prev] in
 	  let proj2 = applistc p2 [t; pred; prev] in
-	    (lift 1 proj2, (n, Some proj1, t) :: subst))
+	    (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
 	(List.rev tys) tl (mkRel 1, [])
-      in ty, ((n, Some last, t) :: subst), constr
+      in ty, (LocalDef (n, last, t) :: subst), constr
 
-  | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
-      ty, ((n, Some b, t) :: subst), lift 1 term
+  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope tl in
+      ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
 let nf_evar_context sigma ctx =
-  List.map (fun (n, b, t) ->
-    (n, Option.map (Evarutil.nf_evar sigma) b, Evarutil.nf_evar sigma t)) ctx
+  List.map (map_constr (Evarutil.nf_evar sigma)) ctx
 
 let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
@@ -923,7 +926,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let argtyp, letbinders, make = telescope binders_rel in
   let argname = Id.of_string "recarg" in
-  let arg = (Name argname, None, argtyp) in
+  let arg = LocalAssum (Name argname, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
@@ -938,7 +941,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       try
 	let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
 	  match ctx, kind_of_term ar with
-	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
+	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
 	      when Reductionops.is_conv env !evdref t u -> t
 	  | _, _ -> error ()
       with e when Errors.noncritical e -> error ()
@@ -958,9 +961,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   in
   let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
-  let wfarg len = (Name argid', None,
-  		   mkSubset (Name argid') argtyp
-		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+  let wfarg len = LocalAssum (Name argid',
+                              mkSubset (Name argid') argtyp
+				       (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
   let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
@@ -974,22 +977,22 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   (* substitute the projection of wfarg for something,
      now intern_arity is in wfarg :: arg *)
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
-  let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
+  let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
   let curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
     let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
-    let lam = (Name (Id.of_string "recproof"), None, rcurry) in
+    let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
     let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
     let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
-      (Name recname, Some body, ty)
+      LocalDef (Name recname, body, ty)
   in
   let fun_bl = intern_fun_binder :: [arg] in
   let lift_lets = Termops.lift_rel_context 1 letbinders in
   let intern_body =
-    let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
+    let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
     let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
@@ -1051,6 +1054,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
 	     evars_typ ctx evars ~hook)
 
 let interp_recursive isfix fixl notations =
+  let open Context.Named.Declaration in
   let env = Global.env() in
   let fixnames = List.map (fun fix -> fix.fix_name) fixl in
 
@@ -1086,8 +1090,8 @@ let interp_recursive isfix fixl notations =
 		 Typing.e_solve_evars env evdref app
 	     with e  when Errors.noncritical e -> t
 	   in
-	     (id,None,fixprot) :: env'
-	 else (id,None,t) :: env')
+	     LocalAssum (id,fixprot) :: env'
+	 else LocalAssum (id,t) :: env')
       [] fixnames fixtypes
   in
   let env_rec = push_named_context rec_sign env in
@@ -1109,7 +1113,7 @@ let interp_recursive isfix fixl notations =
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
-  let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
+  let fixctxnames = List.map (fun (_,ctx) -> List.map get_name ctx) fixctxs in
 
   (* Build the fix declaration block *)
   (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 61a6e1094..5fa51e06e 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -14,14 +14,16 @@ open Vars
 open Entries
 open Declarations
 open Cooking
+open Context.Rel.Declaration
 
 (********************************)
 (* Discharging mutual inductive *)
 
-let detype_param = function
-  | (Name id,None,p) -> id, LocalAssum p
-  | (Name id,Some p,_) -> id, LocalDef p
-  | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable")
+let detype_param =
+  function
+  | LocalAssum (Name id, p) -> id, Entries.LocalAssum p
+  | LocalDef (Name id, p,_) -> id, Entries.LocalDef p
+  | _ -> anomaly (Pp.str "Unnamed inductive local variable")
 
 (* Replace
 
@@ -52,7 +54,7 @@ let abstract_inductive hyps nparams inds =
 (* To be sure to be the same as before, should probably be moved to process_inductive *)
   let params' = let (_,arity,_,_,_) = List.hd inds' in
 		let (params,_) = decompose_prod_n_assum nparams' arity in
-		  List.map detype_param params
+                List.map detype_param params
   in
   let ind'' =
   List.map
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 575e930ea..de7ec61c8 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -23,22 +23,26 @@ open Cases
 open Logic
 open Printer
 open Evd
+open Context.Rel.Declaration
 
 (* This simplifies the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
   let l = ref [] in
-  let contract_context (na,c,t) env =
-    match c with
-      | Some c' when isRel c' ->
+  let contract_context decl env =
+    match decl with
+      | LocalDef (_,c',_) when isRel c' ->
           l := (Vars.substl !l c') :: !l;
           env
       | _ ->
-          let t' = Vars.substl !l t in
-          let c' = Option.map (Vars.substl !l) c in
-          let na' = named_hd env t' na in
+          let t' = Vars.substl !l (get_type decl) in
+          let c' = Option.map (Vars.substl !l) (get_value decl) in
+          let na' = named_hd env t' (get_name decl) in
           l := (mkRel 1) :: List.map (Vars.lift 1) !l;
-          push_rel (na',c',t') env in
+          match c' with
+          | None -> push_rel (LocalAssum (na',t')) env
+          | Some c' -> push_rel (LocalDef (na',c',t')) env
+  in
   let env = process_rel_context contract_context env in
   (env, List.map (Vars.substl !l) lc)
 
@@ -136,9 +140,9 @@ let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags
 
 let pr_db env i =
   try
-    match lookup_rel i env with
-        Name id, _, _ -> pr_id id
-      | Anonymous, _, _ -> str "<>"
+    match lookup_rel i env |> get_name with
+      | Name id -> pr_id id
+      | Anonymous -> str "<>"
   with Not_found -> str "UNBOUND_REL_" ++ int i
 
 let explain_unbound_rel env sigma n =
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index c4ac0e411..251d14af7 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -38,6 +38,7 @@ open Ind_tables
 open Auto_ind_decl
 open Eqschemes
 open Elimschemes
+open Context.Rel.Declaration
 
 (* Flags governing automatic synthesis of schemes *)
 
@@ -463,7 +464,7 @@ let build_combined_scheme env schemes =
   in
   let ctx, _ =
     list_split_rev_at prods
-      (List.rev_map (fun (x, y) -> x, None, y) ctx) in
+      (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
   let typ = it_mkProd_wo_LetIn concl_typ ctx in
   let body = it_mkLambda_or_LetIn concl_bod ctx in
   (body, typ)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 0ea9f959f..0e8d224e4 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -54,7 +54,8 @@ type oblinfo =
 (** Substitute evar references in t using De Bruijn indices,
   where n binders were passed through. *)
 
-let subst_evar_constr evs n idf t = 
+let subst_evar_constr evs n idf t =
+  let open Context.Named.Declaration in
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
@@ -78,9 +79,9 @@ let subst_evar_constr evs n idf t =
 	let args =
 	  let rec aux hyps args acc =
 	     match hyps, args with
-		 ((_, None, _) :: tlh), (c :: tla) ->
+		 (LocalAssum _ :: tlh), (c :: tla) ->
 		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
-	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
+	       | (LocalDef _ :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
@@ -116,22 +117,23 @@ let subst_vars acc n t =
     Changes evars and hypothesis references to variable references.
 *)
 let etype_of_evar evs hyps concl =
+  let open Context.Named.Declaration in
   let rec aux acc n = function
-      (id, copt, t) :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar t in
+      decl :: tl ->
+	let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in
 	let t'' = subst_vars acc 0 t' in
-	let rest, s', trans' = aux (id :: acc) (succ n) tl in
+	let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
 	let trans' = Id.Set.union trans trans' in
-	  (match copt with
-	      Some c -> 
+	  (match decl with
+            | LocalDef (id,c,_) ->
 		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
 		let c' = subst_vars acc 0 c' in
-		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
+		  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
 		Int.Set.union s'' s',
 		Id.Set.union trans'' trans'
-	    | None ->
-		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
+	    | LocalAssum (id,_) ->
+		mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
 	let t', s, trans = subst_evar_constr evs n mkVar concl in
 	  subst_vars acc 0 t', s, trans
@@ -589,15 +591,16 @@ let declare_mutual_definition l =
     Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
     List.iter progmap_remove l; kn
 
-let shrink_body c = 
+let shrink_body c =
+  let open Context.Rel.Declaration in
   let ctx, b = decompose_lam_assum c in
   let b', n, args = 
-    List.fold_left (fun (b, i, args) (n, u, t) ->
+    List.fold_left (fun (b, i, args) decl ->
       if noccurn 1 b then 
 	subst1 mkProp b, succ i, args
       else
-        let args = if Option.is_empty u then mkRel i :: args else args in
-        mkLambda_or_LetIn (n, u, t) b, succ i, args)
+	let args = if is_local_assum decl then mkRel i :: args else args in
+        mkLambda_or_LetIn decl b, succ i, args)
      (b, 1, []) ctx
   in ctx, b', Array.of_list args
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 480e97169..4cf81a250 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -25,6 +25,7 @@ open Constrexpr
 open Constrexpr_ops
 open Goptions
 open Sigma.Notations
+open Context.Rel.Declaration
 
 (********** definition d'un record (structure) **************)
 
@@ -69,16 +70,19 @@ let interp_fields_evars env evars impls_env nots l =
 	| Anonymous -> impls
 	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls
       in
-      let d = (i,b',t') in
+      let d = match b' with
+	      | None -> LocalAssum (i,t')
+	      | Some b' -> LocalDef (i,b',t')
+      in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
       (push_rel d env, impl :: uimpls, d::params, impls))
     (env, [], [], impls_env) nots l
 
 let compute_constructor_level evars env l =
-  List.fold_right (fun (n,b,t as d) (env, univ) ->
+  List.fold_right (fun d (env, univ) ->
     let univ = 
-      if b = None then 
-	let s = Retyping.get_sort_of env evars t in
+      if is_local_assum d then
+	let s = Retyping.get_sort_of env evars (get_type d) in
 	  Univ.sup (univ_of_sort s) univ 
       else univ
     in (push_rel d env, univ)) 
@@ -123,7 +127,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false
   in
   let fullarity = it_mkProd_or_LetIn t' newps in
-  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
+  let env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in
   let env2,impls,newfs,data =
     interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
   in
@@ -151,17 +155,17 @@ let typecheck_params_and_fields def id pl t ps nots fs =
   let newps = Context.Rel.map nf newps in
   let newfs = Context.Rel.map nf newfs in
   let ce t = Evarutil.check_evars env0 Evd.empty evars t in
-    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
-    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
+    List.iter (iter_constr ce) (List.rev newps);
+    List.iter (iter_constr ce) (List.rev newfs);
     Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
 
-let degenerate_decl (na,b,t) =
-  let id = match na with
+let degenerate_decl decl =
+  let id = match get_name decl with
     | Name id -> id
     | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
-  match b with
-    | None -> (id, LocalAssum t)
-    | Some b -> (id, LocalDef b)
+  match decl with
+    | LocalAssum (_,t) -> (id, Entries.LocalAssum t)
+    | LocalDef (_,b,_) -> (id, Entries.LocalDef b)
 
 type record_error =
   | MissingProj of Id.t * Id.t list
@@ -265,23 +269,25 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   in
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,i,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
+      (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
+        let fi = get_name decl in
+        let ti = get_type decl in
 	let (sp_projs,i,subst) =
 	  match fi with
 	  | Anonymous ->
 	      (None::sp_projs,i,NoProjection fi::subst)
 	  | Name fid -> try
 	    let kn, term = 
-	      if optci = None && primitive then 
+	      if is_local_assum decl && primitive then
 		(** Already defined in the kernel silently *)
 		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
 		  Declare.definition_message fid;
 		  kn, mkProj (Projection.make kn false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
-		let body = match optci with
-		  | Some ci -> subst_projection fid subst ci
-		  | None ->
+		let body = match decl with
+		  | LocalDef (_,ci,_) -> subst_projection fid subst ci
+		  | LocalAssum _ ->
 	            (* [ccl] is defined in context [params;x:rp] *)
 		    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
 		    let ccl' = liftn 1 2 ccl in
@@ -323,32 +329,32 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	      let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
 	    end;
-	    let i = if Option.is_empty optci then i+1 else i in
+	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, Option.is_empty optci)::kinds,sp_projs,subst))
+      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
       (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
 let structure_signature ctx =
   let rec deps_to_evar evm l =
     match l with [] -> Evd.empty
-      | [(_,_,typ)] ->
+      | [decl] ->
         let env = Environ.empty_named_context_val in
         let evm = Sigma.Unsafe.of_evar_map evm in
-        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm typ in
+        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
         let evm = Sigma.to_evar_map evm in
         evm
-      | (_,_,typ)::tl ->
+      | decl::tl ->
           let env = Environ.empty_named_context_val in
           let evm = Sigma.Unsafe.of_evar_map evm in
-          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm typ in
+          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
           let evm = Sigma.to_evar_map evm in
 	  let new_tl = Util.List.map_i
-	    (fun pos (n,c,t) -> n,c,
-	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in
+	    (fun pos decl ->
+	       map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
 	  deps_to_evar evm new_tl in
   deps_to_evar Evd.empty (List.rev ctx)
 
@@ -396,7 +402,7 @@ let implicits_of_context ctx =
       | Name n -> Some n
       | Anonymous -> None
     in ExplByPos (i, explname), (true, true, true))
-    1 (List.rev (Anonymous :: (List.map pi1 ctx)))
+    1 (List.rev (Anonymous :: (List.map get_name ctx)))
 
 let declare_class finite def poly ctx id idbuild paramimpls params arity 
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
@@ -409,7 +415,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
   let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
   let impl, projs =
     match fields with
-    | [(Name proj_name, _, field)] when def ->
+    | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
       let class_body = it_mkLambda_or_LetIn field params in
       let _class_type = it_mkProd_or_LetIn arity params in
       let class_entry = 
@@ -450,13 +456,13 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
 			      if b then Backward, pri else Forward, pri) coe)
 	  coers priorities
        in
-       let l = List.map3 (fun (id, _, _) b y -> (id, b, y))
+       let l = List.map3 (fun decl b y -> get_name decl, b, y)
          (List.rev fields) coers (Recordops.lookup_projections ind)
        in IndRef ind, l
   in
   let ctx_context =
-    List.map (fun (na, b, t) ->
-      match Typeclasses.class_of_constr t with
+    List.map (fun decl ->
+      match Typeclasses.class_of_constr (get_type decl) with
       | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
       | None -> None)
       params, params
@@ -478,7 +484,7 @@ let add_constant_class cst =
   let tc = 
     { cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
-      cl_props = [(Anonymous, None, arity)];
+      cl_props = [LocalAssum (Anonymous, arity)];
       cl_projs = [];
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique
@@ -492,8 +498,8 @@ let add_inductive_class ind =
     let ctx = oneind.mind_arity_ctxt in
     let inst = Univ.UContext.instance mind.mind_universes in
     let map = function
-    | (_, Some _, _) -> None
-    | (_, None, t) -> Some (lazy t)
+    | LocalDef _ -> None
+    | LocalAssum (_, t) -> Some (lazy t)
     in
     let args = List.map_filter map ctx in
     let ty = Inductive.type_of_inductive_knowing_parameters
@@ -503,7 +509,7 @@ let add_inductive_class ind =
     in
       { cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
-	cl_props = [Anonymous, None, ty];
+	cl_props = [LocalAssum (Anonymous, ty)];
 	cl_projs = [];
 	cl_strict = !typeclasses_strict;
 	cl_unique = !typeclasses_unique }
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 89e0eb88a..646e2e08a 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -67,7 +67,9 @@ let iter_constructors indsp u fn env nconstr =
     fn (ConstructRef (indsp, i)) env typ
   done
 
-let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ) 
+let iter_named_context_name_type f =
+  let open Context.Named.Declaration in
+  List.iter (fun decl -> f (get_id decl) (get_type decl))
 
 (* General search over hypothesis of a goal *)
 let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
@@ -79,12 +81,13 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
 
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let iter_obj (sp, kn) lobj = match object_tag lobj with
   | "VARIABLE" ->
     begin try
-      let (id, _, typ) = Global.lookup_named (basename sp) in
-      fn (VarRef id) env typ
+      let decl = Global.lookup_named (basename sp) in
+      fn (VarRef (get_id decl)) env (get_type decl)
     with Not_found -> (* we are in a section *) () end
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 60aab09fd..a6a1546ae 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -872,13 +872,14 @@ let vernac_set_end_tac tac =
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables e =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let tys =
     List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
   List.iter (fun id -> 
-    if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
+    if not (List.exists (Id.equal id % get_id) vars) then
       errorlabstrm "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
@@ -1574,6 +1575,7 @@ exception NoHyp
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
 let print_about_hyp_globs ref_or_by_not glnumopt =
+  let open Context.Named.Declaration in
   try
     let gl,id =
       match glnumopt,ref_or_by_not with
@@ -1586,11 +1588,11 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
                            (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
-    let (id,bdyopt,typ) = Context.Named.lookup id hyps in
-    let natureofid = match bdyopt with
-      | None -> "Hypothesis"
-      | Some bdy ->"Constant (let in)" in
-    v 0 (pr_id id ++ str":" ++ pr_constr typ ++ fnl() ++ fnl()
+    let decl = Context.Named.lookup id hyps in
+    let natureofid = match decl with
+                     | LocalAssum _ -> "Hypothesis"
+                     | LocalDef (_,bdy,_) ->"Constant (let in)" in
+    v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
     | NoHyp | Not_found -> print_about ref_or_by_not