CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.

11 files changed, 186 insertions, 155 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index cddc55515f..b29ceb78bd 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 f0c7a39613..0755f8bcfd 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 6bb047af0d..2089bc9443 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 18b2b1444d..02f29b155f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -36,6 +36,7 @@ open Evarconv
 open Indschemes
 open Misctypes
 open Vernacexpr
+open Context.Rel.Declaration
 
 let do_universe poly l = Declare.do_universe poly l
 let do_constraint poly l = Declare.do_constraint poly l
@@ -44,9 +45,9 @@ let rec under_binders env sigma f n c =
   if Int.equal n 0 then snd (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
@@ -259,6 +260,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 = 
@@ -273,7 +275,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
@@ -335,7 +337,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 = {
@@ -378,8 +380,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.
@@ -433,12 +435,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))
@@ -449,7 +451,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 =
@@ -555,8 +557,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
@@ -876,12 +878,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
@@ -890,21 +893,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"];
@@ -918,7 +921,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
@@ -933,7 +936,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 ()
@@ -953,9 +956,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
@@ -969,22 +972,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 
@@ -1046,6 +1049,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
 
@@ -1081,8 +1085,8 @@ let interp_recursive isfix fixl notations =
 		 Typing.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
@@ -1104,7 +1108,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 61a6e10948..5fa51e06e4 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 4a5f14917f..4a145481f7 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 c4ac0e4112..251d14af79 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 0ea9f959f6..0e8d224e42 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 7ae2030343..facc8b75d5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -24,6 +24,7 @@ open Type_errors
 open Constrexpr
 open Constrexpr_ops
 open Goptions
+open Context.Rel.Declaration
 
 (********** definition d'un record (structure) **************)
 
@@ -68,16 +69,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)) 
@@ -122,7 +126,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
@@ -150,17 +154,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
@@ -264,23 +268,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
@@ -322,28 +328,28 @@ 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, _) = Evarutil.new_pure_evar env evm typ in
+        let (evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
         evm
-      | (_,_,typ)::tl ->
+      | decl::tl ->
           let env = Environ.empty_named_context_val in
-          let (evm, ev) = Evarutil.new_pure_evar env evm typ in
+          let (evm, ev) = Evarutil.new_pure_evar env evm (get_type decl) 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)
 
@@ -391,7 +397,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 =
@@ -404,7 +410,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 = 
@@ -445,13 +451,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
@@ -473,7 +479,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
@@ -487,8 +493,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
@@ -498,7 +504,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 89e0eb88ac..646e2e08ac 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 0f81943e2c..8b3e118485 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -871,13 +871,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;
@@ -1568,6 +1569,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
@@ -1580,11 +1582,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