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.

17 files changed, 327 insertions, 231 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6caebf6c4..86b71999b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -324,7 +324,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
-          let hyp = Context.Named.Declaration.map nf decl in
+          let hyp = Context.Named.Declaration.map_constr nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list
 	       (Hint_db.add_list env sigma hintl local_db)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 40c0f7f9b..ea598b61c 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -133,7 +133,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
    fun dir cstr tac gl ->
     let last_hyp_id =
      match Tacmach.pf_hyps gl with
-        (last_hyp_id,_,_)::_ -> last_hyp_id
+        d :: _ -> Context.Named.Declaration.get_id d
       | _ -> (* even the hypothesis id is missing *)
         raise (Logic.RefinerError (Logic.NoSuchHyp !id))
     in
@@ -142,7 +142,8 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
     match gls with
        g::_ ->
         (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
-            (lastid,_,_)::_ ->
+            d ::_ ->
+              let lastid = Context.Named.Declaration.get_id d in
               if not (Id.equal last_hyp_id lastid) then
                begin
                 let gl'' =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c9b2c7cfd..7c05befdd 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -302,8 +302,10 @@ type ('a,'b) optionk2 =
   | Nonek2 of failure
   | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
 
-let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
-  let cty = Evarutil.nf_evar sigma cty in
+let make_resolve_hyp env sigma st flags only_classes pri decl =
+  let open Context.Named.Declaration in
+  let id = get_id decl in
+  let cty = Evarutil.nf_evar sigma (get_type decl) in
   let rec iscl env ty =
     let ctx, ar = decompose_prod_assum ty in
       match kind_of_term (fst (decompose_app ar)) with
@@ -345,9 +347,10 @@ let make_hints g st only_classes sign =
     List.fold_left
     (fun (paths, hints) hyp ->
       let consider =
-	try let (_, b, t) = Global.lookup_named (pi1 hyp) in
+        let open Context.Named.Declaration in
+	try let t = Global.lookup_named (get_id hyp) |> get_type in
 	      (* Section variable, reindex only if the type changed *)
-	      not (Term.eq_constr t (pi3 hyp))
+	      not (Term.eq_constr t (get_type hyp))
 	with Not_found -> true
      in
       if consider then 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c4a23f686..ab6fb37fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -15,6 +15,7 @@ open Reductionops
 open Misctypes
 open Sigma.Notations
 open Proofview.Notations
+open Context.Named.Declaration
 
 (* Absurd *)
 
@@ -47,7 +48,7 @@ let absurd c = absurd c
 let filter_hyp f tac =
   let rec seek = function
     | [] -> Proofview.tclZERO Not_found
-    | (id,_,t)::rest when f t -> tac id
+    | d::rest when f (get_type d) -> tac (get_id d)
     | _::rest -> seek rest in
   Proofview.Goal.enter { enter = begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
@@ -60,8 +61,9 @@ let contradiction_context =
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
       | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
-      | (id,_,typ)::rest ->
-          let typ = nf_evar sigma typ in
+      | d :: rest ->
+          let id = get_id d in
+          let typ = nf_evar sigma (get_type d) in
 	  let typ = whd_betadeltaiota env sigma typ in
 	  if is_empty_type typ then
 	    simplest_elim (mkVar id)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 7767affcc..d441074f6 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -16,6 +16,7 @@ open Tacmach.New
 open Tacticals.New
 open Tactics
 open Proofview.Notations
+open Context.Named.Declaration
 
 (* Supposed to be called without as clause *)
 let introElimAssumsThen tac ba =
@@ -137,7 +138,8 @@ let induction_trailer abs_i abs_j bargs =
           in
 	  let (hyps,_) =
             List.fold_left
-	      (fun (bring_ids,leave_ids) (cid,_,_ as d) ->
+	      (fun (bring_ids,leave_ids) d ->
+                 let cid = get_id d in
                  if not (List.mem cid leave_ids)
                  then (d::bring_ids,leave_ids)
                  else (bring_ids,cid::leave_ids))
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index e0bea7770..a03489c80 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -58,6 +58,7 @@ open Inductiveops
 open Ind_tables
 open Indrec
 open Sigma.Notations
+open Context.Rel.Declaration
 
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
@@ -104,7 +105,7 @@ let get_sym_eq_data env (ind,u) =
     error "Not an inductive type with a single constructor.";
   let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
-  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
+  if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
@@ -139,7 +140,7 @@ let get_non_sym_eq_data env (ind,u) =
     error "Not an inductive type with a single constructor.";
   let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
-  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
+  if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
@@ -173,7 +174,7 @@ let build_sym_scheme env ind =
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
@@ -232,7 +233,7 @@ let build_sym_involutive_scheme env ind =
          (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let c = 
     (my_it_mkLambda_or_LetIn paramsctxt
@@ -352,9 +353,9 @@ let build_l2r_rew_scheme dep env ind kind =
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
   let realsign_ind_P =
-    name_context env ((Name varH,None,applied_ind_P)::realsign_P) in
+    name_context env ((LocalAssum (Name varH,applied_ind_P))::realsign_P) in
   let realsign_ind_G =
-    name_context env ((Name varH,None,applied_ind_G)::
+    name_context env ((LocalAssum (Name varH,applied_ind_G))::
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
@@ -465,9 +466,9 @@ let build_l2r_forward_rew_scheme dep env ind kind =
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let realsign_ind_P n aP =
-    name_context env ((Name varH,None,aP)::realsign_P n) in
+    name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
   let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
@@ -545,7 +546,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
@@ -599,9 +600,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
   | hp :: p :: ind :: indargs ->
      let c' = 
       my_it_mkLambda_or_LetIn indargs
-	(mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p)
-	  (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp)
-	    (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind)
+        (mkLambda_or_LetIn (map_constr (liftn (-1) 1) p)
+	  (mkLambda_or_LetIn (map_constr (liftn (-1) 2) hp)
+	    (mkLambda_or_LetIn (map_constr (lift 2) ind)
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
 	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
@@ -737,10 +738,10 @@ let build_congr env (eq,refl,ctx) ind =
   let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
   let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
-  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
+  if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context arityctxt env in
-  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
+  let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1e814e861..d27dcd82a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -43,6 +43,7 @@ open Misctypes
 open Sigma.Notations
 open Proofview.Notations
 open Unification
+open Context.Named.Declaration
 
 (* Options *)
 
@@ -960,7 +961,7 @@ let apply_on_clause (f,t) clause =
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (e,None,t) env in
+  let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
   let discriminator =
     build_discriminator e_env sigma dirn (mkVar e) sort cpath in
   let sigma,(pf, absurd_term), eff = 
@@ -1064,7 +1065,7 @@ let make_tuple env sigma (rterm,rty) lind =
   assert (dependent (mkRel lind) rty);
   let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
   let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
-  let (na,_,_) = lookup_rel lind env in
+  let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
   (* Now [lind] is [mkRel 1] and we abstract on (na:a) *)
@@ -1335,7 +1336,7 @@ let simplify_args env sigma t =
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (e, None,t) env in
+  let e_env = push_named (LocalAssum (e,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
@@ -1612,14 +1613,14 @@ let unfold_body x =
   Proofview.Goal.enter { enter = begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let (_, xval, _) = Context.Named.lookup x hyps in
+  let xval = Context.Named.lookup x hyps |> get_value in
   let xval = match xval with
   | None -> errorlabstrm "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | Some xval -> pf_nf_evar gl xval
   in
   afterHyp x begin fun aft ->
-  let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun d cl -> (get_id d, InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   let reducth h = Proofview.V82.tactic (fun gl -> reduct_in_hyp rfun h gl) in
@@ -1636,9 +1637,10 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
 exception FoundHyp of (Id.t * constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
-let is_eq_x gl x (id,_,c) =
+let is_eq_x gl x d =
+  let id = get_id d in
   try
-    let c = pf_nf_evar gl c in
+    let c = pf_nf_evar gl (get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
     if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
     if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1655,11 +1657,12 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   (* The set of hypotheses using x *)
   let dephyps =
-    List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
+    List.rev (snd (List.fold_right (fun dcl (deps,allhyps) ->
+      let id = get_id dcl in
       if not (Id.equal id hyp)
          && List.exists (fun y -> occur_var_in_decl env y dcl) deps
       then
-        ((if b = None then deps else id::deps), id::allhyps)
+        ((if is_local_assum dcl then deps else id::deps), id::allhyps)
       else
         (deps,allhyps))
       hyps
@@ -1683,7 +1686,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
 let subst_one_var dep_proof_ok x =
   Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
-    let (_,xval,_) = pf_get_hyp x gl in
+    let xval = pf_get_hyp x gl |> get_value in
     (* If x has a body, simply replace x with body and clear x *)
     if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else
       (* x is a variable: *)
@@ -1742,14 +1745,14 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
-    let test (hyp,_,c) =
+    let test decl =
       try
-        let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+        let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match kind_of_term x, kind_of_term y with
         | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z))  ->
-            Some hyp
+            Some (get_id decl)
         | _ ->
             None
       with Constr_matching.PatternMatchingFailure -> None
@@ -1763,7 +1766,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
-    let (_,_,c) = pf_get_hyp hyp gl in
+    let c = pf_get_hyp hyp gl |> get_type in
     let _,_,(_,x,y) = find_eq_data_decompose c in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if Term.eq_constr x y then Proofview.tclUNIT () else
@@ -1831,10 +1834,11 @@ let cond_eq_term c t gl =
 let rewrite_assumption_cond cond_eq_term cl =
   let rec arec hyps gl = match hyps with
     | [] -> error "No such assumption."
-    | (id,_,t) ::rest ->
+    | hyp ::rest ->
+        let id = get_id hyp in
 	begin
 	  try
-            let dir = cond_eq_term t gl in
+            let dir = cond_eq_term (get_type hyp) gl in
 	    general_rewrite_clause dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 97b5ba0cc..f443837a4 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -16,6 +16,7 @@ open Evd
 open Locus
 open Sigma.Notations
 open Proofview.Notations
+open Context.Named.Declaration
 
 (* The instantiate tactic *)
 
@@ -43,14 +44,14 @@ let instantiate_tac n c ido =
 	    match hloc with
 		InHyp ->
 		  (match decl with
-		      (_,None,typ) -> evar_list typ
+                    | LocalAssum (_,typ) -> evar_list typ
 		    | _ -> error
 			"Please be more specific: in type or value?")
 	      | InHypTypeOnly ->
-		  let (_, _, typ) = decl in evar_list typ
+		  evar_list (get_type decl)
 	      | InHypValueOnly ->
 		  (match decl with
-		      (_,Some body,_) -> evar_list body
+		    | LocalDef (_,body,_) -> evar_list body
 		    | _ -> error "Not a defined hypothesis.") in
   if List.length evl < n then
     error "Not enough uninstantiated existential variables.";
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c99e591fe..730da147a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -34,6 +34,7 @@ open Tacred
 open Printer
 open Vernacexpr
 open Sigma.Notations
+open Context.Named.Declaration
 
 (****************************************)
 (* General functions                    *)
@@ -727,11 +728,12 @@ let make_resolves env sigma flags pri poly ?name cr =
   ents
 
 (* used to add an hypothesis to the local hint database *)
-let make_resolve_hyp env sigma (hname,_,htyp) =
+let make_resolve_hyp env sigma decl =
+  let hname = get_id decl in
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (mkVar hname, htyp, Univ.ContextSet.empty)]
+       (mkVar hname, get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
@@ -1061,7 +1063,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
 	(* Not clever enough to construct dependency graph of evars *)
 	error "Not clever enough to deal with evars dependent in other evars.";
       raise (Found (c,t))
-    | _ -> iter_constr find_next_evar c in
+    | _ -> Constr.iter find_next_evar c in
   let rec iter c =
     try find_next_evar c; c
     with Found (evar,t) ->
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 29d848ca1..bcec90f80 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -19,6 +19,7 @@ open Constr_matching
 open Coqlib
 open Declarations
 open Tacmach.New
+open Context.Rel.Declaration
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -101,13 +102,16 @@ let match_with_one_constructor style onlybinary allow_rec t =
 	      (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
 	  if
 	    List.for_all
-	      (fun (_,b,c) -> Option.is_empty b && isRel c && Int.equal (destRel c) mib.mind_nparams) ctx
+	      (fun decl -> let c = get_type decl in
+	                   is_local_assum decl &&
+			   isRel c &&
+                           Int.equal (destRel c) mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
 	else
 	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
-	  let cargs = List.map pi3 ((prod_assum ctyp)) in
+	  let cargs = List.map get_type (prod_assum ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod ctyp then
 	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
@@ -152,7 +156,7 @@ let is_tuple t =
 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)
+    | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
     | _ -> false) 0 lc
 
 let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ded1e8076..9bfbbc41b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -28,6 +28,7 @@ open Misctypes
 open Tacexpr
 open Sigma.Notations
 open Proofview.Notations
+open Context.Named.Declaration
 
 let clear hyps = Proofview.V82.tactic (clear hyps)
 
@@ -181,9 +182,9 @@ let make_inv_predicate env evd indf realargs id status concl =
 let dependent_hyps env id idlist gl =
   let rec dep_rec =function
     | [] -> []
-    | (id1,_,_)::l ->
+    | d::l ->
 	(* Update the type of id1: it may have been subject to rewriting *)
-	let d = pf_get_hyp id1 gl in
+	let d = pf_get_hyp (get_id d) gl in
 	if occur_var_in_decl env id d
         then d :: dep_rec l
         else dep_rec l
@@ -192,8 +193,8 @@ let dependent_hyps env id idlist gl =
 
 let split_dep_and_nodep hyps gl =
   List.fold_right
-    (fun (id,_,_ as d) (l1,l2) ->
-       if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2))
+    (fun d (l1,l2) ->
+       if var_occurs_in_pf gl (get_id d) then (d::l1,l2) else (l1,d::l2))
     hyps ([],[])
 
 (* Computation of dids is late; must have been done in rewrite_equations*)
@@ -296,8 +297,8 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
       error "Discarding pattern not allowed for inversion equations."
   | IntroAction (IntroRewrite _) ->
       error "Rewriting pattern not allowed for inversion equations."
-  | IntroAction (IntroOrAndPattern (IntroAndPattern [] | IntroOrPattern [[]])) when allow_conj -> (None, [])
-  | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ]))
+  | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, [])
+  | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l)))
       when allow_conj -> (Some id,l)
   | IntroAction (IntroOrAndPattern (IntroAndPattern _)) ->
       if issimple then
@@ -384,7 +385,7 @@ let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
   let first_eq = ref MoveLast in
-  let avoid = if as_mode then List.map pi1 nodepids else [] in
+  let avoid = if as_mode then List.map get_id nodepids else [] in
   match othin with
     | Some thin ->
         tclTHENLIST
@@ -399,11 +400,11 @@ let rewrite_equations as_mode othin neqns names ba =
 		 (onLastHypId (fun id ->
 		   tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
 	       names;
-	     tclMAP (fun (id,_,_) -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
-               let idopt = if as_mode then Some id else None in
+	     tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
+               let idopt = if as_mode then Some (get_id d) else None in
 	       intro_move idopt (if thin then MoveLast else !first_eq))
 	       nodepids;
-	     (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)]
+	     (tclMAP (fun d -> tclTRY (clear [get_id d])) depids)]
     | None ->
         (* simple inversion *)
         if as_mode then
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cdf38ae46..70782ec64 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -27,6 +27,7 @@ open Tacticals.New
 open Tactics
 open Decl_kinds
 open Proofview.Notations
+open Context.Named.Declaration
 
 let no_inductive_inconstr env sigma constr =
   (str "Cannot recognize an inductive predicate in " ++
@@ -117,11 +118,11 @@ let rec add_prods_sign env sigma t =
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (id,None,c1) env) sigma b'
+        add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
+        add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates whether the inversion lemma is dependent or not.
@@ -154,7 +155,8 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let ivars = global_vars env i in
       let revargs,ownsign =
 	fold_named_context
-	  (fun env (id,_,_ as d) (revargs,hyps) ->
+	  (fun env d (revargs,hyps) ->
+             let id = get_id d in
              if Id.List.mem id ivars then
 	       ((mkVar id)::revargs, Context.Named.add d hyps)
 	     else
@@ -166,7 +168,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
-  let extenv = push_named (p,None,npty) env in
+  let extenv = push_named (LocalAssum (p,npty)) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -203,8 +205,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let global_named_context = Global.named_context () in
   let ownSign = ref begin
     fold_named_context
-      (fun env (id,_,_ as d) sign ->
-         if mem_named_context id global_named_context then sign
+      (fun env d sign ->
+         if mem_named_context (get_id d) global_named_context then sign
 	 else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
   end in
@@ -217,9 +219,9 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
-	ownSign := Context.Named.add (h,None,ty) !ownSign;
+	ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign;
 	applist (mkVar h, inst)
-    | _ -> map_constr fill_holes c
+    | _ -> Constr.map fill_holes c
   in
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 29002af9e..b39e34fc1 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -36,6 +36,7 @@ open Termops
 open Libnames
 open Sigma.Notations
 open Proofview.Notations
+open Context.Named.Declaration
 
 (** Typeclass-based generalized rewriting. *)
 
@@ -134,6 +135,7 @@ module GlobalBindings (M : sig
   val arrow : evars -> evars * constr
 end) = struct
   open M
+  open Context.Rel.Declaration
   let relation : evars -> evars * constr = find_global (fst relation) (snd relation)
 
   let reflexive_type = find_global relation_classes "Reflexive"
@@ -219,8 +221,8 @@ end) = struct
 	    let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
 	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
 	  else
-	    let (evars, b, arg, cstrs) = 
-	      aux (Environ.push_rel (na, None, ty) env) evars b cstrs 
+	    let (evars, b, arg, cstrs) =
+	      aux (Environ.push_rel (LocalAssum (na, ty)) env) evars b cstrs
 	    in
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
 	    let pred = mkLambda (na, ty, b) in
@@ -318,7 +320,7 @@ end) = struct
 	    let evars, rb = aux evars env b' (pred n) in
 	      app_poly env evars pointwise_relation [| ty; b'; rb |]
 	  else
-	    let evars, rb = aux evars (Environ.push_rel (na, None, ty) env) b (pred n) in
+	    let evars, rb = aux evars (Environ.push_rel (LocalAssum (na, ty)) env) b (pred n) in
 	      app_poly env evars forall_relation
 		[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
 	| _ -> raise Not_found
@@ -469,6 +471,7 @@ let rec decompose_app_rel env evd t =
   | _ -> error "Cannot find a relation to rewrite."
 
 let decompose_applied_relation env sigma (c,l) =
+  let open Context.Rel.Declaration in
   let ctype = Retyping.get_type_of env sigma c in
   let find_rel ty =
     let sigma, cl = Clenv.make_evar_clause env sigma ty in
@@ -491,7 +494,7 @@ let decompose_applied_relation env sigma (c,l) =
     | Some c -> c
     | None ->
 	let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
-	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> n, None, t) ctx)) with
+	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
 	| Some c -> c
 	| None -> error "Cannot find an homogeneous relation to rewrite."
 
@@ -766,9 +769,9 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
       in
 	Environ.push_named
-	  (Id.of_string "do_subrelation", 
-	   Some (snd (app_poly_sort b env evars dosub [||])), 
-	   snd (app_poly_nocheck env evars appsub [||]))
+	  (LocalDef (Id.of_string "do_subrelation",
+	             snd (app_poly_sort b env evars dosub [||]),
+	             snd (app_poly_nocheck env evars appsub [||])))
 	  env
     in
     let evars, morph = new_cstr_evar evars env' app in
@@ -1110,8 +1113,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       (* 	    | _ -> b') *)
 
       | Lambda (n, t, b) when flags.under_lambdas ->
-	let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
-	let env' = Environ.push_rel (n', None, t) env in
+        let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
+        let open Context.Rel.Declaration in
+	let env' = Environ.push_rel (LocalAssum (n', t)) env in
 	let bty = Retyping.get_type_of env' (goalevars evars) b in
 	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
 	let state, b' = s.strategy { state ; env = env' ; unfresh ;
@@ -1495,8 +1499,8 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 (** Insert a declaration after the last declaration it depends on *)
 let rec insert_dependent env decl accu hyps = match hyps with
 | [] -> List.rev_append accu [decl]
-| (id, _, _  as ndecl) :: rem ->
-  if occur_var_in_decl env id decl then
+| ndecl :: rem ->
+  if occur_var_in_decl env (get_id ndecl) decl then
     List.rev_append accu (decl :: hyps)
   else
     insert_dependent env decl (ndecl :: accu) rem
@@ -1506,16 +1510,19 @@ let assert_replacing id newt tac =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let ctx = Environ.named_context env in
-    let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in
+    let after, before = List.split_when (Id.equal id % get_id) ctx in
     let nc = match before with
     | [] -> assert false
-    | (id, b, _) :: rem -> insert_dependent env (id, None, newt) [] after @ rem
+    | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
       let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
       let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
-      let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
+      let map d =
+        let n = get_id d in
+        if Id.equal n id then ev' else mkVar n
+      in
       let (e, _) = destEvar ev in
       Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
     end }
@@ -1543,7 +1550,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	    assert_replacing id newt tac
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (id, None, newt)
+            convert_hyp_no_check (LocalAssum (id, newt))
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
             Proofview.Goal.enter { enter = begin fun gl ->
@@ -2053,7 +2060,8 @@ let setoid_proof ty fn fallback =
         try
           let rel, _, _ = decompose_app_rel env sigma concl in
           let evm = sigma in
-          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in
+          let open Context.Rel.Declaration in
+          let car = get_type (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in
 	    (try init_setoid () with _ -> raise Not_found);
             fn env sigma car rel
         with e -> Proofview.tclZERO e
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1112da4a0..30a9071fd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -42,6 +42,7 @@ open Tacintern
 open Taccoerce
 open Sigma.Notations
 open Proofview.Notations
+open Context.Named.Declaration
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
@@ -444,14 +445,13 @@ let interp_reference ist env sigma = function
     try try_interp_ltac_var (coerce_to_reference env) ist (Some (env,sigma)) (loc, id)
     with Not_found ->
       try
-        let (v, _, _) = Environ.lookup_named id env in
-        VarRef v
+        VarRef (get_id (Environ.lookup_named id env))
       with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
   match v with
-  | (_, Some _, _) -> EvalVarRef id
+  | LocalDef _ -> EvalVarRef id
   | _ -> error_not_evaluable (VarRef id)
 
 let interp_evaluable ist env sigma = function
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index 80786058d..2144b75e7 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -11,6 +11,7 @@
 
 open Names
 open Tacexpr
+open Context.Named.Declaration
 
 (** [t] is the type of matching successes. It ultimately contains a
     {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
@@ -278,9 +279,10 @@ module PatternMatching (E:StaticEnvironment) = struct
       [hyps]. Tries the hypotheses in order. For each success returns
       the name of the matched hypothesis. *)
   let hyp_match_type hypname pat hyps =
-    pick hyps >>= fun (id,b,hyp) ->
-    let refresh = not (Option.is_empty b) in
-    pattern_match_term refresh pat hyp () <*>
+    pick hyps >>= fun decl ->
+    let id = get_id decl in
+    let refresh = is_local_def decl in
+    pattern_match_term refresh pat (get_type decl) () <*>
     put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
     return id
 
@@ -290,12 +292,12 @@ module PatternMatching (E:StaticEnvironment) = struct
       success returns the name of the matched hypothesis. *)
   let hyp_match_body_and_type hypname bodypat typepat hyps =
     pick hyps >>= function
-      | (id,Some body,hyp) ->
+      | LocalDef (id,body,hyp) ->
           pattern_match_term false bodypat body () <*>
           pattern_match_term true typepat hyp () <*>
           put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
           return id
-      | (id,None,hyp) -> fail
+      | LocalAssum (id,hyp) -> fail
 
   (** [hyp_match pat hyps] dispatches to
       {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether
@@ -317,7 +319,7 @@ module PatternMatching (E:StaticEnvironment) = struct
         (* spiwack: alternatively it is possible to return the list
            with the matched hypothesis removed directly in
            [hyp_match]. *)
-        let select_matched_hyp (id,_,_) = Id.equal id matched_hyp in
+        let select_matched_hyp decl = Id.equal (get_id decl) matched_hyp in
         let hyps = CList.remove_first select_matched_hyp hyps in
         hyp_pattern_list_match pats hyps lhs
     | [] -> return lhs
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d79de4913..7f904a561 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,6 +16,7 @@ open Declarations
 open Tacmach
 open Clenv
 open Sigma.Notations
+open Context.Named.Declaration
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -69,7 +70,7 @@ let nthDecl m gl =
   try List.nth (pf_hyps gl) (m-1)
   with Failure _ -> error "No such assumption."
 
-let nthHypId m gl = pi1 (nthDecl m gl)
+let nthHypId m gl = nthDecl m gl |> get_id
 let nthHyp m gl   = mkVar (nthHypId m gl)
 
 let lastDecl gl   = nthDecl 1 gl
@@ -80,7 +81,7 @@ let nLastDecls n gl =
   try List.firstn n (pf_hyps gl)
   with Failure _ -> error "Not enough hypotheses in the goal."
 
-let nLastHypsId n gl = List.map pi1 (nLastDecls n gl)
+let nLastHypsId n gl = List.map get_id (nLastDecls n gl)
 let nLastHyps n gl   = List.map mkVar (nLastHypsId n gl)
 
 let onNthDecl m tac gl  = tac (nthDecl m gl) gl
@@ -98,7 +99,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
 let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 
 let afterHyp id gl =
-  fst (List.split_when (fun (hyp,_,_) -> Id.equal hyp id) (pf_hyps gl))
+  fst (List.split_when (Id.equal id % get_id) (pf_hyps gl))
 
 (***************************************)
 (*           Clause Tacticals          *)
@@ -552,8 +553,7 @@ module New = struct
   let nthHypId m gl =
     (** We only use [id] *)
     let gl = Proofview.Goal.assume gl in
-    let (id,_,_) = nthDecl m gl in
-    id
+    nthDecl m gl |> get_id
   let nthHyp m gl = 
     mkVar (nthHypId m gl)
 
@@ -585,7 +585,7 @@ module New = struct
   let afterHyp id tac =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
-    let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in
+    let rem, _ = List.split_when (Id.equal id % get_id) hyps in
     tac rem
     end }
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aeb3726a0..8f30df5c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -161,19 +161,21 @@ let _ =
 
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
-let unsafe_intro env store (id, c, t) b =
+let unsafe_intro env store decl b =
+  let open Context.Named.Declaration in
   Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let ctx = named_context_val env in
-    let nctx = push_named_context_val (id, c, t) ctx in
-    let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
+    let nctx = push_named_context_val decl ctx in
+    let inst = List.map (mkVar % get_id) (named_context env) in
     let ninst = mkRel 1 :: inst in
-    let nb = subst1 (mkVar id) b in
+    let nb = subst1 (mkVar (get_id decl)) b in
     let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
-    Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
+    Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn decl ev, sigma)
   end }
 
 let introduction ?(check=true) id =
+  let open Context.Named.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
@@ -186,8 +188,8 @@ let introduction ?(check=true) id =
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
-    | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
-    | LetIn (_, c, t, b) -> unsafe_intro env store (id, Some c, t) b
+    | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
+    | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
     | _ -> raise (RefinerError IntroNeedsProduct)
   end }
 
@@ -296,6 +298,7 @@ let move_hyp id dest gl = Tacmach.move_hyp id dest gl
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
+  let open Context.Named.Declaration in
   let fold accu (src, dst) = match accu with
   | None -> None
   | Some (srcs, dsts) ->
@@ -317,7 +320,7 @@ let rename_hyp repl =
       let concl = Proofview.Goal.concl gl in
       let store = Proofview.Goal.extra gl in
       (** Check that we do not mess variables *)
-      let fold accu (id, _, _) = Id.Set.add id accu in
+      let fold accu decl = Id.Set.add (get_id decl) accu in
       let vars = List.fold_left fold Id.Set.empty hyps in
       let () =
         if not (Id.Set.subset src vars) then
@@ -335,14 +338,14 @@ let rename_hyp repl =
       let make_subst (src, dst) = (src, mkVar dst) in
       let subst = List.map make_subst repl in
       let subst c = Vars.replace_vars subst c in
-      let map (id, body, t) =
-        let id = try List.assoc_f Id.equal id repl with Not_found -> id in
-        (id, Option.map subst body, subst t)
+      let map decl =
+        decl |> map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
+             |> map_constr subst
       in
       let nhyps = List.map map hyps in
       let nconcl = subst concl in
       let nctx = Environ.val_of_named_context nhyps in
-      let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
+      let instance = List.map (mkVar % get_id) hyps in
       Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
         let sigma = Sigma.to_evar_map sigma in
         let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
@@ -370,11 +373,13 @@ let id_of_name_with_default id = function
 let default_id_of_sort s =
   if Sorts.is_small s then default_small_ident else default_type_ident
 
-let default_id env sigma = function
-  | (name,None,t) ->
+let default_id env sigma decl =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (name,t) ->
       let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in
       id_of_name_with_default dft name
-  | (name,Some b,_) -> id_of_name_using_hdchar env b name
+  | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name
 
 (* Non primitive introduction tactics are treated by intro_then_gen
    There is possibly renaming, with possibly names to avoid and
@@ -409,8 +414,9 @@ let find_name mayrepl decl naming gl = match naming with
 (**************************************************************)
 
 let assert_before_then_gen b naming t tac =
+  let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let id = find_name b (Anonymous,None,t) naming gl in
+    let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
     Tacticals.New.tclTHENLAST
       (Proofview.V82.tactic
          (fun gl ->
@@ -427,8 +433,9 @@ let assert_before na = assert_before_gen false (naming_of_name na)
 let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
 
 let assert_after_then_gen b naming t tac =
+  let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
-    let id = find_name b (Anonymous,None,t) naming gl in
+    let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
     Tacticals.New.tclTHENFIRST
       (Proofview.V82.tactic
          (fun gl ->
@@ -472,17 +479,18 @@ let cofix ido gl = match ido with
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-let pf_reduce_decl redfun where (id,c,ty) gl =
+let pf_reduce_decl redfun where decl gl =
+  let open Context.Named.Declaration in
   let redfun' = Tacmach.pf_reduce redfun gl in
-  match c with
-  | None ->
+  match decl with
+  | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
 	errorlabstrm "" (pr_id id ++ str " has no value.");
-      (id,None,redfun' ty)
-  | Some b ->
+      LocalAssum (id,redfun' ty)
+  | LocalDef (id,b,ty) ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
       let ty' =	if where != InHypValueOnly then redfun' ty else ty in
-      (id,Some b',ty')
+      LocalDef (id,b',ty')
 
 (* Possibly equip a reduction with the occurrences mentioned in an
    occurrence clause *)
@@ -568,19 +576,20 @@ let reduct_option ?(check=false) redfun = function
 
 (** Tactic reduction modulo evars (for universes essentially) *)
 
-let pf_e_reduce_decl redfun where (id,c,ty) gl =
+let pf_e_reduce_decl redfun where decl gl =
+  let open Context.Named.Declaration in
   let sigma = project gl in
   let redfun = redfun (pf_env gl) in
-  match c with
-  | None ->
+  match decl with
+  | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
 	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma, ty' = redfun sigma ty in
-      sigma, (id,None,ty')
-  | Some b ->
+      sigma, LocalAssum (id,ty')
+  | LocalDef (id,b,ty) ->
       let sigma, b' = if where != InHypTypeOnly then redfun sigma b else sigma, b in
       let sigma, ty' = if where != InHypValueOnly then redfun sigma ty else sigma, ty in
-	sigma, (id,Some b',ty')
+	sigma, LocalDef (id,b',ty')
 
 let e_reduct_in_concl (redfun,sty) gl =
   Proofview.V82.of_tactic
@@ -609,21 +618,22 @@ let e_change_in_concl (redfun,sty) =
     Sigma.Unsafe.of_pair (convert_concl_no_check c sty, sigma)
   end }
 
-let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
-  match c with
-  | None ->
+let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
+  let open Context.Named.Declaration in
+  match decl with
+  | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
 	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma',ty' = redfun false env sigma ty in
-      sigma', (id,None,ty')
-  | Some b ->
+      sigma', LocalAssum (id,ty')
+  | LocalDef (id,b,ty) ->
       let sigma',b' = 
 	if where != InHypTypeOnly then redfun true env sigma b else sigma, b 
       in
       let sigma',ty' = 
 	if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty 
       in
-	sigma', (id,Some b',ty')
+	sigma', LocalDef (id,b',ty')
 
 let e_change_in_hyp redfun (id,where) =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -767,10 +777,9 @@ let unfold_constr = function
 let find_intro_names ctxt gl =
   let _, res = List.fold_right
     (fun decl acc ->
-      let wantedname,x,typdecl = decl in
       let env,idl = acc in
       let name = fresh_id idl (default_id env gl.sigma decl) gl in
-      let newenv = push_rel (wantedname,x,typdecl) env in
+      let newenv = push_rel decl env in
       (newenv,(name::idl)))
     ctxt (pf_env gl , []) in
   List.rev res
@@ -782,15 +791,16 @@ let build_intro_tac id dest tac = match dest with
      Proofview.V82.tactic (move_hyp id dest); tac id]
     
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
+  let open Context.Rel.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     let concl = nf_evar (Tacmach.New.project gl) concl in
     match kind_of_term concl with
     | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        let name = find_name false (name,None,t) name_flag gl in
+        let name = find_name false (LocalAssum (name,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        let name = find_name false (name,Some b,t) name_flag gl in
+        let name = find_name false (LocalDef (name,b,t)) name_flag gl in
 	build_intro_tac name move_flag tac
     | _ ->
 	begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
@@ -853,21 +863,24 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
   aux n []
 
 let get_next_hyp_position id gl =
+  let open Context.Named.Declaration in
   let rec aux = function
   | [] -> raise (RefinerError (NoSuchHyp id))
-  | (hyp,_,_) :: right ->
-    if Id.equal hyp id then
-      match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
+  | decl :: right ->
+    if Id.equal (get_id decl) id then
+      match right with decl::_ -> MoveBefore (get_id decl) | [] -> MoveLast
     else
       aux right
   in
   aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
 let get_previous_hyp_position id gl =
+  let open Context.Named.Declaration in
   let rec aux dest = function
   | [] -> raise (RefinerError (NoSuchHyp id))
-  | (hyp,_,_) :: right ->
-    if Id.equal hyp id then dest else aux (MoveAfter hyp) right
+  | decl :: right ->
+      let hyp = get_id decl in
+      if Id.equal hyp id then dest else aux (MoveAfter hyp) right
   in
   aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
@@ -1146,6 +1159,7 @@ let index_of_ind_arg t =
   in aux None 0 t
 
 let enforce_prop_bound_names rename tac =
+  let open Context.Rel.Declaration in
   match rename with
   | Some (isrec,nn) when Namegen.use_h_based_elimination_names () ->
       (* Rename dependent arguments in Prop with name "H" *)
@@ -1165,11 +1179,11 @@ let enforce_prop_bound_names rename tac =
                 Name (add_suffix Namegen.default_prop_ident s)
               else
                 na in
-            mkProd (na,t,aux (push_rel (na,None,t) env) sigma (i-1) t')
+            mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t')
         | Prod (Anonymous,t,t') ->
-            mkProd (Anonymous,t,aux (push_rel (Anonymous,None,t) env) sigma (i-1) t')
+            mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t')
         | LetIn (na,c,t,t') ->
-            mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t')
+            mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
         | _ -> print_int i; Pp.msg (print_constr t); assert false in
       let rename_branch i =
         Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -1391,11 +1405,13 @@ type conjunction_status =
   | NotADefinedRecordUseScheme of constr
 
 let make_projection env sigma params cstr sign elim i n c u =
+  let open Context.Rel.Declaration in
   let elim = match elim with
   | NotADefinedRecordUseScheme elim ->
       (* bugs: goes from right to left when i increases! *)
-      let (na,b,t) = List.nth cstr.cs_args i in
-      let b = match b with None -> mkRel (i+1) | Some b -> b in
+      let decl = List.nth cstr.cs_args i in
+      let t = get_type decl in
+      let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in
       let branch = it_mkLambda_or_LetIn b cstr.cs_args in
       if
 	(* excludes dependent projection types *)
@@ -1651,6 +1667,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
 
 let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     id (clear_flag,(loc,(d,lbind))) tac =
+  let open Context.Rel.Declaration in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
@@ -1658,7 +1675,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
   let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
-  let targetid = find_name true (Anonymous,None,t') naming gl in
+  let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
   let rec aux idstoclear with_destruct c =
     Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -1770,13 +1787,15 @@ let exact_proof c gl =
   in tclTHEN (tclEVARUNIVCONTEXT ctx) (Tacmach.refine_no_check c) gl
 
 let assumption =
+  let open Context.Named.Declaration in
   let rec arec gl only_eq = function
   | [] ->
     if only_eq then
       let hyps = Proofview.Goal.hyps gl in
       arec gl false hyps
     else Tacticals.New.tclZEROMSG (str "No such assumption.")
-  | (id, c, t)::rest ->
+  | decl::rest ->
+    let t = get_type decl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let (sigma, is_same_type) =
@@ -1787,7 +1806,7 @@ let assumption =
     in
     if is_same_type then
       (Proofview.Unsafe.tclEVARS sigma) <*>
-	Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar id) h }
+	Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
     else arec gl only_eq rest
   in
   let assumption_tac = { enter = begin fun gl ->
@@ -1822,40 +1841,43 @@ let check_is_type env ty msg =
   with e when Errors.noncritical e ->
     msg e
 
-let check_decl env (_, c, ty) msg =
+let check_decl env decl msg =
+  let open Context.Named.Declaration in
+  let ty = get_type decl in
   Proofview.tclEVARMAP >>= fun sigma ->
   let evdref = ref sigma in
   try
     let _ = Typing.sort_of env evdref ty in
-    let _ = match c with
-    | None -> ()
-    | Some c -> Typing.check env evdref c ty
+    let _ = match decl with
+    | LocalAssum _ -> ()
+    | LocalDef (_,c,_) -> Typing.check env evdref c ty
     in
     Proofview.Unsafe.tclEVARS !evdref
   with e when Errors.noncritical e ->
     msg e
 
 let clear_body ids =
+  let open Context.Named.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     let ctx = named_context env in
-    let map (id, body, t as decl) = match body with
-    | None ->
+    let map = function
+    | LocalAssum (id,t) as decl ->
       let () = if List.mem_f Id.equal id ids then
         errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
       in
       decl
-    | Some _ ->
-      if List.mem_f Id.equal id ids then (id, None, t) else decl
+    | LocalDef (id,_,t) as decl ->
+      if List.mem_f Id.equal id ids then LocalAssum (id, t) else decl
     in
     let ctx = List.map map ctx in
     let base_env = reset_context env in
     let env = push_named_context ctx base_env in
     let check_hyps =
-      let check env (id, _, _ as decl) =
+      let check env decl =
         let msg _ = Tacticals.New.tclZEROMSG
-          (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids)
+          (str "Hypothesis " ++ pr_id (get_id decl) ++ on_the_bodies ids)
         in
         check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env)
       in
@@ -1897,11 +1919,13 @@ let rec intros_clearing = function
 (* Keeping only a few hypotheses *)
 
 let keep hyps =
+  let open Context.Named.Declaration in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   Proofview.tclENV >>= fun env ->
   let ccl = Proofview.Goal.concl gl in
   let cl,_ =
-    fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
+    fold_named_context_reverse (fun (clear,keep) decl ->
+      let hyp = get_id decl in
       if Id.List.mem hyp hyps
         || List.exists (occur_var_in_decl env hyp) keep
 	|| occur_var env hyp ccl
@@ -2442,20 +2466,24 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
   end }
 
 let insert_before decls lasthyp env =
+  let open Context.Named.Declaration in
   match lasthyp with
   | None -> push_named_context decls env
   | Some id ->
   Environ.fold_named_context
-    (fun _ (id',_,_ as d) env ->
-      let env = if Id.equal id id' then push_named_context decls env else env in
+    (fun _ d env ->
+      let env = if Id.equal id (get_id d) then push_named_context decls env else env in
       push_named d env)
     ~init:(reset_context env) env
 
 (* unsafe *)
 
 let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
-  let body = if dep then Some c else None in
+  let open Context.Named.Declaration in
   let t = match ty with Some t -> t | _ -> typ_of env sigma c in
+  let decl = if dep then LocalDef (id,c,t)
+	     else LocalAssum (id,t)
+  in
   match with_eq with
   | Some (lr,(loc,ido)) ->
       let heq = match ido with
@@ -2471,11 +2499,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
-      let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in
+      let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
       let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in
       Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r)
   | None ->
-      let newenv = insert_before [id,body,t] lastlhyp env in
+      let newenv = insert_before [decl] lastlhyp env in
       let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in
       Sigma (mkNamedLetIn id c t x, sigma, p)
 
@@ -2557,12 +2585,17 @@ let generalized_name c t ids cl = function
    but only those at [occs] in [T] *)
 
 let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
+  let open Context.Rel.Declaration in
   let decls,cl = decompose_prod_n_assum i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in
   let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name c t ids cl' na in
-  mkProd_or_LetIn (na,b,t) cl', sigma'
+  let decl = match b with
+    | None -> LocalAssum (na,t)
+    | Some b -> LocalDef (na,b,t)
+  in
+  mkProd_or_LetIn decl cl', sigma'
 
 let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   let env = Tacmach.pf_env gl in
@@ -2571,18 +2604,19 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   generalize_goal_gen env sigma ids i o t cl
 
 let generalize_dep ?(with_let=false) c gl =
+  let open Context.Named.Declaration in
   let env = pf_env gl in
   let sign = pf_hyps gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
-  let seek d toquant =
-    if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
+  let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) =
+    if List.exists (fun d' -> occur_var_in_decl env (get_id d') d) toquant
       || dependent_in_decl c d then
       d::toquant
     else
       toquant in
   let to_quantify = Context.Named.fold_outside seek sign ~init:[] in
   let to_quantify_rev = List.rev to_quantify in
-  let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
+  let qhyps = List.map get_id to_quantify_rev in
   let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
@@ -2594,7 +2628,7 @@ let generalize_dep ?(with_let=false) c gl =
   let body =
     if with_let then
       match kind_of_term c with
-      | Var id -> pi2 (Tacmach.pf_get_hyp gl id)
+      | Var id -> Tacmach.pf_get_hyp gl id |> get_value
       | _ -> None
     else None
   in
@@ -2720,14 +2754,15 @@ let specialize (c,lbind) =
 (* The two following functions should already exist, but found nowhere *)
 (* Unfolds x by its definition everywhere *)
 let unfold_body x gl =
+  let open Context.Named.Declaration in
   let hyps = pf_hyps gl in
   let xval =
     match Context.Named.lookup x hyps with
-        (_,Some xval,_) -> xval
+      | LocalDef (_,xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
@@ -3041,6 +3076,7 @@ exception Shunt of Id.t move_location
 let cook_sign hyp0_opt inhyps indvars env =
   (* First phase from L to R: get [toclear], [decldep] and [statuslist]
      for the hypotheses before (= more ancient than) hyp0 (see above) *)
+  let open Context.Named.Declaration in
   let toclear = ref [] in
   let avoid = ref [] in
   let decldeps = ref [] in
@@ -3049,7 +3085,8 @@ let cook_sign hyp0_opt inhyps indvars env =
   let lstatus = ref [] in
   let before = ref true in
   let maindep = ref false in
-  let seek_deps env (hyp,_,_ as decl) rhyp =
+  let seek_deps env decl rhyp =
+    let hyp = get_id decl in
     if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false)
     then begin
       before:=false;
@@ -3068,7 +3105,7 @@ let cook_sign hyp0_opt inhyps indvars env =
       in
       let depother = List.is_empty inhyps &&
 	(List.exists (fun id -> occur_var_in_decl env id decl) indvars ||
-         List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps)
+         List.exists (fun decl' -> occur_var_in_decl env (get_id decl') decl) !decldeps)
       in
       if not (List.is_empty inhyps) && Id.List.mem hyp inhyps
          || dephyp0 || depother
@@ -3090,7 +3127,8 @@ let cook_sign hyp0_opt inhyps indvars env =
   in
   let _ = fold_named_context seek_deps env ~init:MoveFirst in
   (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
-  let compute_lstatus lhyp (hyp,_,_) =
+  let compute_lstatus lhyp decl =
+    let hyp = get_id decl in
     if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then
       raise (Shunt lhyp);
     if Id.List.mem hyp !ldeps then begin
@@ -3280,6 +3318,7 @@ let mk_term_eq env sigma ty t ty' t' =
     mkHEq ty t ty' t', mkHRefl ty' t'
 
 let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
+  let open Context.Rel.Declaration in
   Proofview.Refine.refine { run = begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
@@ -3291,9 +3330,13 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   in
     (* Abstract by equalities *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
-  let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
+  let abseqs = it_mkProd_or_LetIn (lift eqslen abshypeq) (List.map (fun x -> LocalAssum (Anonymous, x)) eqs) in
+  let decl = match body with
+    | None -> LocalAssum (Name id, c)
+    | Some body -> LocalDef (Name id, body, c)
+  in
     (* Abstract by the "generalized" hypothesis. *)
-  let genarg = mkProd_or_LetIn (Name id, body, c) abseqs in
+  let genarg = mkProd_or_LetIn decl abseqs in
     (* Abstract by the extension of the context *)
   let genctyp = it_mkProd_or_LetIn genarg ctx in
     (* The goal will become this product. *)
@@ -3309,11 +3352,13 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   end }
 
 let hyps_of_vars env sign nogen hyps =
+  let open Context.Named.Declaration in
   if Id.Set.is_empty hyps then []
   else
     let (_,lh) =
       Context.Named.fold_inside
-        (fun (hs,hl) (x,_,_ as d) ->
+        (fun (hs,hl) d ->
+          let x = get_id d in
 	  if Id.Set.mem x nogen then (hs,hl)
 	  else if Id.Set.mem x hs then (hs,x::hl)
 	  else
@@ -3342,11 +3387,12 @@ let linear vars args =
       true
     with Seen -> false
 
-let is_defined_variable env id = match lookup_named id env with
-| (_, None, _) -> false
-| (_, Some _, _) -> true
+let is_defined_variable env id =
+  let open Context.Named.Declaration in
+  lookup_named id env |> is_local_def
 
 let abstract_args gl generalize_vars dep id defined f args =
+  let open Context.Rel.Declaration in
   let sigma = ref (Tacmach.project gl) in
   let env = Tacmach.pf_env gl in
   let concl = Tacmach.pf_concl gl in
@@ -3363,9 +3409,10 @@ let abstract_args gl generalize_vars dep id defined f args =
        eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
     *)
   let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
-    let (name, _, ty), arity =
+    let name, ty, arity =
       let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
-	List.hd rel, c
+      let decl = List.hd rel in
+      get_name decl, get_type decl, c
     in
     let argty = Tacmach.pf_unsafe_type_of gl arg in
     let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
@@ -3379,7 +3426,7 @@ let abstract_args gl generalize_vars dep id defined f args =
       	  Id.Set.add id nongenvars, Id.Set.remove id vars, env)
       | _ ->
 	  let name = get_id name in
-	  let decl = (Name name, None, ty) in
+	  let decl = LocalAssum (Name name, ty) in
 	  let ctx = decl :: ctx in
 	  let c' = mkApp (lift 1 c, [|mkRel 1|]) in
 	  let args = arg :: args in
@@ -3430,15 +3477,15 @@ let abstract_args gl generalize_vars dep id defined f args =
     else None
 
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
+  let open Context.Named.Declaration in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   Coqlib.check_required_library Coqlib.jmeq_module_name;
   let (f, args, def, id, oldid) =
     let oldid = Tacmach.New.pf_get_new_id id gl in
-    let (_, b, t) = Tacmach.New.pf_get_hyp id gl in
-      match b with
-      | None -> let f, args = decompose_app t in
+      match Tacmach.New.pf_get_hyp id gl with
+      | LocalAssum (_,t) -> let f, args = decompose_app t in
 	        (f, args, false, id, oldid)
-      | Some t ->
+      | LocalDef (_,t,_) ->
 	  let f, args = decompose_app t in
 	  (f, args, true, id, oldid)
   in
@@ -3473,6 +3520,7 @@ let rec compare_upto_variables x y =
   else compare_constr compare_upto_variables x y
 
 let specialize_eqs id gl =
+  let open Context.Rel.Declaration in
   let env = Tacmach.pf_env gl in
   let ty = Tacmach.pf_get_hyp_typ gl id in
   let evars = ref (project gl) in
@@ -3501,15 +3549,14 @@ let specialize_eqs id gl =
 	    if in_eqs then acc, in_eqs, ctx, ty
 	    else
 	      let e = e_new_evar (push_rel_context ctx env) evars t in
-		aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+		aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
     | t -> acc, in_eqs, ctx, ty
   in
   let acc, worked, ctx, ty = aux false [] (mkVar id) ty in
   let ctx' = nf_rel_context_evar !evars ctx in
-  let ctx'' = List.map (fun (n,b,t as decl) ->
-    match b with
-    | Some k when isEvar k -> (n,None,t)
-    | b -> decl) ctx'
+  let ctx'' = List.map (function
+    | LocalDef (n,k,t) when isEvar k -> LocalAssum (n,t)
+    | decl -> decl) ctx'
   in
   let ty' = it_mkProd_or_LetIn ty ctx'' in
   let acc' = it_mkLambda_or_LetIn acc ctx'' in
@@ -3543,18 +3590,19 @@ let occur_rel n c =
    We also return the conclusion.
 *)
 let decompose_paramspred_branch_args elimt =
-  let rec cut_noccur elimt acc2 : Context.Rel.t * Context.Rel.t * types =
+  let open Context.Rel.Declaration in
+  let rec cut_noccur elimt acc2 =
     match kind_of_term elimt with
       | Prod(nme,tpe,elimt') ->
 	  let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in
 	  if not (occur_rel 1 elimt') && isRel hd_tpe
-	  then cut_noccur elimt' ((nme,None,tpe)::acc2)
+	  then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2)
 	  else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
       | App(_, _) | Rel _ -> acc2 , [] , elimt
       | _ -> error_ind_scheme "" in
-  let rec cut_occur elimt acc1 : Context.Rel.t * Context.Rel.t * Context.Rel.t * types =
+  let rec cut_occur elimt acc1 =
     match kind_of_term elimt with
-      | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1)
+      | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c (LocalAssum (nme,tpe)::acc1)
       | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
       | App(_, _) | Rel _ -> acc1,[],[],elimt
       | _ -> error_ind_scheme "" in
@@ -3596,6 +3644,7 @@ let exchange_hd_app subst_hd t =
 
    - finish to fill in the elim_scheme: indarg/farg/args and finally indref. *)
 let compute_elim_sig ?elimc elimt =
+  let open Context.Rel.Declaration in
   let params_preds,branches,args_indargs,conclusion =
     decompose_paramspred_branch_args elimt in
 
@@ -3629,8 +3678,8 @@ let compute_elim_sig ?elimc elimt =
     (* 3- Look at last arg: is it the indarg? *)
     ignore (
       match List.hd args_indargs with
-	| hiname,Some _,hi -> error_ind_scheme ""
-	| hiname,None,hi ->
+	| LocalDef (hiname,_,hi) -> error_ind_scheme ""
+	| LocalAssum (hiname,hi) ->
 	    let hi_ind, hi_args = decompose_app hi in
 	    let hi_is_ind = (* hi est d'un type globalisable *)
 	      match kind_of_term hi_ind with
@@ -3654,24 +3703,25 @@ let compute_elim_sig ?elimc elimt =
   with Exit -> (* Ending by computing indref: *)
     match !res.indarg with
       | None -> !res (* No indref *)
-      | Some ( _,Some _,_) -> error_ind_scheme ""
-      | Some ( _,None,ind) ->
+      | Some (LocalDef _) -> error_ind_scheme ""
+      | Some (LocalAssum (_,ind)) ->
 	  let indhd,indargs = decompose_app ind in
 	  try {!res with indref = Some (global_of_constr indhd) }
 	  with e when Errors.noncritical e ->
             error "Cannot find the inductive type of the inductive scheme."
 
 let compute_scheme_signature scheme names_info ind_type_guess =
+  let open Context.Rel.Declaration in
   let f,l = decompose_app scheme.concl in
   (* Vérifier que les arguments de Qi sont bien les xi. *)
   let cond, check_concl =
     match scheme.indarg with
-      | Some (_,Some _,_) ->
+      | Some (LocalDef _) ->
 	  error "Strange letin, cannot recognize an induction scheme."
       | None -> (* Non standard scheme *)
 	  let cond hd = Term.eq_constr hd ind_type_guess && not scheme.farg_in_concl
 	  in (cond, fun _ _ -> ())
-      | Some ( _,None,ind) -> (* Standard scheme from an inductive type *)
+      | Some (LocalAssum (_,ind)) -> (* Standard scheme from an inductive type *)
 	  let indhd,indargs = decompose_app ind in
 	  let cond hd = Term.eq_constr hd indhd in
 	  let check_concl is_pred p =
@@ -3703,7 +3753,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
   in
   let rec find_branches p lbrch =
     match lbrch with
-      | (_,None,t)::brs ->
+      | LocalAssum (_,t) :: brs ->
 	(try
 	   let lchck_brch = check_branch p t in
 	   let n = List.fold_left
@@ -3716,7 +3766,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	       lchck_brch in
 	   (avoid,namesign) :: find_branches (p+1) brs
 	 with Exit-> error_ind_scheme "the branches of")
-      | (_,Some _,_)::_ -> error_ind_scheme "the branches of"
+      | LocalDef _ :: _ -> error_ind_scheme "the branches of"
       | [] -> check_concl is_pred p; []
   in
   Array.of_list (find_branches 0 (List.rev scheme.branches))
@@ -3797,13 +3847,15 @@ let is_functional_induction elimc gl =
 (* Wait the last moment to guess the eliminator so as to know if we
    need a dependent one or not *)
 
-let get_eliminator elim dep s gl = match elim with
+let get_eliminator elim dep s gl =
+  let open Context.Rel.Declaration in
+  match elim with
   | ElimUsing (elim,indsign) ->
       Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
       let _, (l, s) = compute_elim_signature elims id in
-      let branchlengthes = List.map (fun (_,b,c) -> assert (b=None); pi1 (decompose_prod_letin c)) (List.rev s.branches) in
+      let branchlengthes = List.map (fun d -> assert (is_local_assum d); pi1 (decompose_prod_letin (get_type d))) (List.rev s.branches) in
       evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l
 
 (* Instantiate all meta variables of elimclause using lid, some elts
@@ -3864,6 +3916,7 @@ let induction_tac with_evars params indvars elim gl =
    induction applies with the induction hypotheses *)
 
 let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
+  let open Context.Named.Declaration in
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
@@ -3876,7 +3929,7 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
     let s = Retyping.get_sort_family_of env sigma tmpcl in
     let deps_cstr =
       List.fold_left
-        (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
+        (fun a decl -> if is_local_assum decl then (mkVar (get_id decl))::a else a) [] deps in
     let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in
     let branchletsigns =
       let f (_,is_not_let,_,_) = is_not_let in
@@ -3956,6 +4009,7 @@ let induction_without_atomization isrec with_evars elim names lid =
 
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls gl =
+  let open Context.Named.Declaration in
   if occur_var (Tacmach.pf_env gl) id (Tacmach.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
   then errorlabstrm ""
@@ -3963,7 +4017,8 @@ let clear_unselected_context id inhyps cls gl =
      ++ str ".");
   match cls.onhyps with
   | Some hyps ->
-      let to_erase (id',_,_ as d) =
+      let to_erase d =
+        let id' = get_id d in
 	if Id.List.mem id' inhyps then (* if selected, do not erase *) None
 	else
 	  (* erase if not selected and dependent on id or selected hyps *)
@@ -4536,39 +4591,45 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
    is solved by tac *)
 
 (** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl evd d1 d2 = match d2,d1 with
-  | (_,Some _,_), (_,None,_) -> false
-  | (_,Some b1,t1), (_,Some b2,t2) -> 
+let interpretable_as_section_decl evd d1 d2 =
+  let open Context.Named.Declaration in
+  match d2, d1 with
+  | LocalDef _, LocalAssum _ -> false
+  | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
     e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
-  | (_,None,t1), (_,_,t2) -> e_eq_constr_univs evd t1 t2
+  | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (get_type d2)
 
 let rec decompose len c t accu =
+  let open Context.Rel.Declaration in
   if len = 0 then (c, t, accu)
   else match kind_of_term c, kind_of_term t with 
   | Lambda (na, u, c), Prod (_, _, t) ->
-    decompose (pred len) c t ((na, None, u) :: accu)
+    decompose (pred len) c t (LocalAssum (na, u) :: accu)
   | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
-    decompose (pred len) c t ((na, Some b, u) :: accu)
+    decompose (pred len) c t (LocalDef (na, b, u) :: accu)
   | _ -> assert false
 
-let rec shrink ctx sign c t accu = match ctx, sign with
-| [], [] -> (c, t, accu)
-| p :: ctx, (id, _, _) :: sign ->
-  if noccurn 1 c then
-    let c = subst1 mkProp c in
-    let t = subst1 mkProp t in
-    shrink ctx sign c t accu
-  else
-    let c = mkLambda_or_LetIn p c in
-    let t = mkProd_or_LetIn p t in
-    let accu = match p with
-    | (_, None, _) -> mkVar id :: accu
-    | (_, Some _, _) -> accu
+let rec shrink ctx sign c t accu =
+  let open Context.Rel.Declaration in
+  match ctx, sign with
+  | [], [] -> (c, t, accu)
+  | p :: ctx, decl :: sign ->
+      if noccurn 1 c then
+        let c = subst1 mkProp c in
+        let t = subst1 mkProp t in
+        shrink ctx sign c t accu
+      else
+        let c = mkLambda_or_LetIn p c in
+        let t = mkProd_or_LetIn p t in
+        let accu = if is_local_assum p then let open Context.Named.Declaration in
+                                            mkVar (get_id decl) :: accu
+                                       else accu
     in
     shrink ctx sign c t accu
 | _ -> assert false
 
 let shrink_entry sign const =
+  let open Context.Named.Declaration in
   let open Entries in
   let typ = match const.const_entry_type with
   | None -> assert false
@@ -4589,6 +4650,7 @@ let abstract_subproof id gk tac =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
+  let open Context.Named.Declaration in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let current_sign = Global.named_context()
@@ -4597,7 +4659,8 @@ let abstract_subproof id gk tac =
   let evdref = ref sigma in
   let sign,secsign =
     List.fold_right
-      (fun (id,_,_ as d) (s1,s2) ->
+      (fun d (s1,s2) ->
+        let id = get_id d in
 	if mem_named_context id current_sign &&
           interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
         then (s1,push_named_context_val d s2)