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.

4 files changed, 139 insertions, 104 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 8f8b29d10..f1f65bd8a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -16,6 +16,7 @@ open Vars
 open Termops
 open Environ
 open Globnames
+open Context.Named.Declaration
 
 (** Generic filters *)
 module Filter :
@@ -230,20 +231,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id,_,_ as d) :: ctxt ->
+  | true :: filter, d :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
       if test_id d c then instrec filter ctxt (succ i)
-      else (id, c) :: instrec filter ctxt (succ i)
+      else (get_id d, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id,_,_ as d) =
+     let map i d =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (id,c)
+        if test_id d c then None else Some (get_id d, c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +252,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (fun (id,_,_) -> isVarId id) info args
+  evar_instance_array (isVarId % get_id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -660,7 +661,7 @@ let restrict evk filter ?candidates evd =
       evar_extra = Store.empty } in
   let evar_names = reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
+  let id_inst = Array.map_of_list (mkVar % get_id) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
@@ -722,10 +723,10 @@ let evars_of_term c =
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
-  List.fold_right (fun (_, b, t) s ->
+  List.fold_right (fun decl s ->
     Option.fold_left (fun s t ->
       Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term t)) b)
+      (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl))
     nc Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
@@ -1228,8 +1229,9 @@ let pr_meta_map mmap =
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
-let pr_decl ((id,b,_),ok) =
-  match b with
+let pr_decl (decl,ok) =
+  let id = get_id decl in
+  match get_value decl with
   | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
   | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
       print_constr c ++ str (if ok then ")" else "}")
@@ -1346,8 +1348,9 @@ let print_env_short env =
   let pr_body n = function
   | None -> pr_name n
   | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
-  let pr_named_decl (n, b, _) = pr_body (Name n) b in
-  let pr_rel_decl (n, b, _) = pr_body n b in
+  let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in
+  let pr_rel_decl decl = let open Context.Rel.Declaration in
+                         pr_body (get_name decl) (get_value decl) in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
diff --git a/engine/namegen.ml b/engine/namegen.ml
index fc3f0cc75..6b2b58531 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -22,6 +22,7 @@ open Libnames
 open Globnames
 open Environ
 open Termops
+open Context.Rel.Declaration
 
 (**********************************************************************)
 (* Conventional names *)
@@ -113,7 +114,7 @@ let hdchar env c =
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
-	   try match Environ.lookup_rel (n-k) env with
+	   try match Environ.lookup_rel (n-k) env |> to_tuple with
 	     | (Name id,_,_)   -> lowercase_first_char id
 	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
@@ -142,10 +143,9 @@ let prod_name = mkProd_name
 let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
 let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
 
-let name_assumption env (na,c,t) =
-  match c with
-    | None      -> (named_hd env t na, None, t)
-    | Some body -> (named_hd env body na, c, t)
+let name_assumption env = function
+    | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
+    | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
 
 let name_context env hyps =
   snd
@@ -277,11 +277,12 @@ let next_name_away = next_name_away_with_default default_non_dependent_string
 let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
-    (fun (na,c,t) newenv ->
+    (fun decl newenv ->
+       let (na,_,t) = to_tuple decl in
        let na = named_hd newenv t na in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
-       push_rel (Name id,c,t) newenv)
+       push_rel (set_name (Name id) decl) newenv)
     env
 
 (* 5- Looks for next fresh name outside a list; avoids also to use names that
diff --git a/engine/termops.ml b/engine/termops.ml
index b7d89ba7b..f698f8151 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -15,6 +15,9 @@ open Term
 open Vars
 open Environ
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (* Sorts and sort family *)
 
 let print_sort = function
@@ -98,26 +101,28 @@ let print_constr_env t = !term_printer t
 let print_constr t = !term_printer (Global.env()) t
 let set_print_constr f = term_printer := f
 
-let pr_var_decl env (id,c,typ) =
-  let pbody = match c with
-    | None ->  (mt ())
-    | Some c ->
+let pr_var_decl env decl =
+  let open NamedDecl in
+  let pbody = match decl with
+    | LocalAssum _ ->  mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env typ in
+  let pt = print_constr_env env (get_type decl) in
   let ptyp = (str" : " ++ pt) in
-    (pr_id id ++ hov 0 (pbody ++ ptyp))
+    (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
-let pr_rel_decl env (na,c,typ) =
-  let pbody = match c with
-    | None -> mt ()
-    | Some c ->
+let pr_rel_decl env decl =
+  let open RelDecl in
+  let pbody = match decl with
+    | LocalAssum _ -> mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env typ in
-    match na with
+  let ptyp = print_constr_env env (get_type decl) in
+    match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
 
@@ -157,42 +162,53 @@ let rel_list n m =
   in
   reln [] 1
 
-let push_rel_assum (x,t) env = push_rel (x,None,t) env
+let push_rel_assum (x,t) env =
+  let open RelDecl in
+  push_rel (LocalAssum (x,t)) env
 
 let push_rels_assum assums =
-  push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
+  let open RelDecl in
+  push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums)
 
 let push_named_rec_types (lna,typarray,_) env =
+  let open NamedDecl in
   let ctxt =
     Array.map2_i
       (fun i na t ->
 	 match na with
-	   | Name id -> (id, None, lift i t)
+	   | Name id -> LocalAssum (id, lift i t)
 	   | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
       lna typarray in
   Array.fold_left
     (fun e assum -> push_named assum e) env ctxt
 
 let lookup_rel_id id sign =
+  let open RelDecl in
   let rec lookrec n = function
-    | []                     -> raise Not_found
-    | (Anonymous, _, _) :: l -> lookrec (n + 1) l
-    | (Name id', b, t) :: l  ->
-      if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l
+    | [] ->
+        raise Not_found
+    | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l ->
+        lookrec (n + 1) l
+    | LocalAssum (Name id', t) :: l  ->
+        if Names.Id.equal id' id then (n,None,t)  else lookrec (n + 1) l
+    | LocalDef (Name id', b, t) :: l  ->
+        if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l
   in
   lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na, t, c)
-    | Some b -> mkLetIn (na, b, t, c)
+let mkProd_or_LetIn decl c =
+  let open RelDecl in
+  match decl with
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
-let mkProd_wo_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na,  t, c)
-    | Some b -> subst1 b c
+let mkProd_wo_LetIn decl c =
+  let open RelDecl in
+  match decl with
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (_,b,_) -> subst1 b c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
@@ -208,10 +224,11 @@ let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_Le
 let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
 
 let it_mkLambda_or_LetIn_from_no_LetIn c decls =
+  let open RelDecl in
   let rec aux k decls c = match decls with
   | [] -> c
-  | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
-  | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c)
+  | LocalDef (na,b,t) :: decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
+  | LocalAssum (na,t) :: decls -> mkLambda (na,t,aux (k-1) decls c)
   in aux (List.length decls) (List.rev decls) c
 
 (* *)
@@ -302,7 +319,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    (co-)fixpoint) *)
 
 let fold_rec_types g (lna,typarray,_) e =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -317,7 +334,9 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+let map_constr_with_binders_left_to_right g f l c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) -> 
@@ -327,18 +346,18 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (na,None,t) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (na,None,t) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (na,Some bo,t) l) b in
+      let b' = f (g (LocalDef (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
@@ -379,7 +398,9 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
 	else mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
-let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
+let map_constr_with_full_binders g f l cstr =
+  let open RelDecl in
+  match kind_of_term cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> cstr
   | Cast (c,k, t) ->
@@ -388,16 +409,16 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (na,None,t) l) c in
+      let c' = f (g (LocalAssum (na,t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (na,None,t) l) c in
+      let c' = f (g (LocalAssum (na,t)) l) c in
       if t==t' && c==c' then cstr else  mkLambda (na, t', c')
   | LetIn (na,b,t,c) ->
       let b' = f l b in
       let t' = f l t in
-      let c' = f (g (na,Some b,t) l) c in
+      let c' = f (g (LocalDef (na,b,t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -418,7 +439,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -426,7 +447,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -439,23 +460,25 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_full_binders g f n acc c = match kind_of_term c with
+let fold_constr_with_full_binders g f n acc c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
@@ -467,23 +490,25 @@ let fold_constr_with_binders g f n acc c =
    each binder traversal; it is not recursive and the order with which
    subterms are processed is not specified *)
 
-let iter_constr_with_full_binders g f l c = match kind_of_term c with
+let iter_constr_with_full_binders g f l c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
   | Cast (c,_, t) -> f l c; f l t
-  | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+  | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+  | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+  | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
   | App (c,args) -> f l c; Array.iter (f l) args
   | Proj (p,c) -> f l c
   | Evar (_,args) -> Array.iter (f l) args
   | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
   | Fix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
   | CoFix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
 
@@ -531,10 +556,11 @@ let occur_var env id c =
   in
   try occur_rec c; false with Occur -> true
 
-let occur_var_in_decl env hyp (_,c,typ) =
-  match c with
-    | None -> occur_var env hyp typ
-    | Some body ->
+let occur_var_in_decl env hyp decl =
+  let open NamedDecl in
+  match decl with
+    | LocalAssum (_,typ) -> occur_var env hyp typ
+    | LocalDef (_, body, typ) ->
         occur_var env hyp typ ||
         occur_var env hyp body
 
@@ -593,10 +619,11 @@ let dependent_no_evar = dependent_main true false
 let dependent_univs = dependent_main false true
 let dependent_univs_no_evar = dependent_main true true
 
-let dependent_in_decl a (_,c,t) =
-  match c with
-    | None -> dependent a t
-    | Some body -> dependent a body || dependent a t
+let dependent_in_decl a decl =
+  let open NamedDecl in
+  match decl with
+    | LocalAssum (_,t) -> dependent a t
+    | LocalDef (_, body, t) -> dependent a body || dependent a t
 
 let count_occurrences m t =
   let n = ref 0 in
@@ -699,10 +726,10 @@ let replace_term = replace_term_gen eq_constr
 
 let vars_of_env env =
   let s =
-    Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s)
+    Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s)
       (named_context env) ~init:Id.Set.empty in
   Context.Rel.fold_outside
-    (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
+    (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
 
 let add_vname vars = function
@@ -728,11 +755,11 @@ let empty_names_context = []
 
 let ids_of_rel_context sign =
   Context.Rel.fold_outside
-    (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+    (fun decl l -> match RelDecl.get_name decl with Name id -> id::l | Anonymous -> l)
     sign ~init:[]
 
 let ids_of_named_context sign =
-  Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[]
+  Context.Named.fold_outside (fun decl idl -> NamedDecl.get_id decl :: idl) sign ~init:[]
 
 let ids_of_context env =
   (ids_of_rel_context (rel_context env))
@@ -740,7 +767,7 @@ let ids_of_context env =
 
 
 let names_of_rel_context env =
-  List.map (fun (na,_,_) -> na) (rel_context env)
+  List.map RelDecl.get_name (rel_context env)
 
 let is_section_variable id =
   try let _ = Global.lookup_named id in true
@@ -813,7 +840,7 @@ let filtering env cv_pb c1 c2 =
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
 	  aux env cv_pb t1 t2;
-	  aux ((n,None,t1)::env) cv_pb c1 c2
+	  aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
@@ -826,8 +853,8 @@ let filtering env cv_pb c1 c2 =
 
 let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
   let rec prodec_rec i l c = match kind_of_term c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) ((n,None,t)::l) c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
     | Cast (c,_,_)    -> prodec_rec i l c
     | _               -> i,l,c in
   prodec_rec 0 []
@@ -902,16 +929,16 @@ let process_rel_context f env =
 
 let assums_of_rel_context sign =
   Context.Rel.fold_outside
-    (fun (na,c,t) l ->
-      match c with
-          Some _ -> l
-        | None -> (na, t)::l)
+    (fun decl l ->
+      match decl with
+      | RelDecl.LocalDef _ -> l
+      | RelDecl.LocalAssum (na,t) -> (na, t)::l)
     sign ~init:[]
 
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
     | d::sign ->
-	aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign
+	aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
     | [] ->
 	acc
   in
@@ -919,7 +946,7 @@ let map_rel_context_in_env f env sign =
 
 let map_rel_context_with_binders f sign =
   let rec aux k = function
-    | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign
+    | d::sign -> RelDecl.map_constr (f k) d :: aux (k-1) sign
     | [] -> []
   in
   aux (Context.Rel.length sign) sign
@@ -933,21 +960,23 @@ let lift_rel_context n =
 let smash_rel_context sign =
   let rec aux acc = function
   | [] -> acc
-  | (_,None,_ as d) :: l -> aux (d::acc) l
-  | (_,Some b,_) :: l ->
+  | (RelDecl.LocalAssum _ as d) :: l -> aux (d::acc) l
+  | RelDecl.LocalDef (_,b,_) :: l ->
       (* Quadratic in the number of let but there are probably a few of them *)
       aux (List.rev (substl_rel_context [b] (List.rev acc))) l
   in List.rev (aux [] sign)
 
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
-let rec mem_named_context id = function
-  | (id',_,_) :: _ when Id.equal id id' -> true
+let rec mem_named_context id ctxt =
+  match ctxt with
+  | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
 let compact_named_context_reverse sign =
-  let compact l (i1,c1,t1) =
+  let compact l decl =
+    let (i1,c1,t1) = NamedDecl.to_tuple decl in
     match l with
     | [] -> [[i1],c1,t1]
     | (l2,c2,t2)::q ->
@@ -959,16 +988,17 @@ let compact_named_context_reverse sign =
 let compact_named_context sign = List.rev (compact_named_context_reverse sign)
 
 let clear_named_body id env =
+  let open NamedDecl in
   let aux _ = function
-  | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t)
+  | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t))
   | d -> push_named d in
   fold_named_context aux env ~init:(reset_context env)
 
 let global_vars env ids = Id.Set.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
-  | (_,None,t) -> global_vars_set env t
-  | (_,Some c,t) ->
+  | NamedDecl.LocalAssum (_,t) -> global_vars_set env t
+  | NamedDecl.LocalDef (_,c,t) ->
       Id.Set.union (global_vars_set env t)
         (global_vars_set env c)
 
@@ -976,7 +1006,8 @@ let dependency_closure env sign hyps =
   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 = NamedDecl.get_id d in
           if Id.Set.mem x hs then
             (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
             x::hl)
@@ -996,7 +1027,7 @@ let on_judgment_type f j = { j with uj_type = f j.uj_type }
 let context_chop k ctx =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
-    | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
+    | (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t)
     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
     | (_, []) -> anomaly (Pp.str "context_chop")
   in chop_aux [] (k,ctx)
diff --git a/engine/termops.mli b/engine/termops.mli
index 720ed3bd6..c2a4f3323 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -101,7 +101,7 @@ val occur_evar : existential_key -> types -> bool
 val occur_var : env -> Id.t -> types -> bool
 val occur_var_in_decl :
   env ->
-  Id.t -> 'a * types option * types -> bool
+  Id.t -> Context.Named.Declaration.t -> bool
 val free_rels : constr -> Int.Set.t
 
 (** [dependent m t] tests whether [m] is a subterm of [t] *)