CLEANUP: minor readability improvements

mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.

If multiple modules define a function with a same name, e.g.:

	Context.{Rel,Named}.get_type

those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.

12 files changed, 103 insertions, 98 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6e01a676a..8c43ac8b5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -32,6 +32,8 @@ open Misctypes
 open Proofview.Notations
 open Hints
 
+module NamedDecl = Context.Named.Declaration
+
 (** Hint database named "typeclass_instances", now created directly in Auto *)
 
 (** Options handling *)
@@ -523,9 +525,8 @@ let evars_to_goals p evm =
 
 (** Making local hints  *)
 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 id = NamedDecl.get_id decl in
+  let cty = Evarutil.nf_evar sigma (NamedDecl.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
@@ -564,10 +565,9 @@ let make_hints g st only_classes sign =
     List.fold_left
       (fun hints hyp ->
         let consider =
-          let open Context.Named.Declaration in
-          try let t = Global.lookup_named (get_id hyp) |> get_type in
+          try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in
               (* Section variable, reindex only if the type changed *)
-              not (Term.eq_constr t (get_type hyp))
+              not (Term.eq_constr t (NamedDecl.get_type hyp))
           with Not_found -> true
         in
         if consider then
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c3796b484..c81705c1a 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -13,7 +13,8 @@ open Coqlib
 open Reductionops
 open Misctypes
 open Proofview.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (* Absurd *)
 
@@ -46,7 +47,7 @@ let absurd c = absurd c
 let filter_hyp f tac =
   let rec seek = function
     | [] -> Proofview.tclZERO Not_found
-    | d::rest when f (get_type d) -> tac (get_id d)
+    | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.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,8 @@ let contradiction_context =
     let rec seek_neg l = match l with
       | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | d :: rest ->
-          let id = get_id d in
-          let typ = nf_evar sigma (get_type d) in
+          let id = NamedDecl.get_id d in
+          let typ = nf_evar sigma (NamedDecl.get_type d) in
 	  let typ = whd_all 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 f2b9eec4b..3f0c01a29 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -16,7 +16,8 @@ open Tacmach.New
 open Tacticals.New
 open Tactics
 open Proofview.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (* Supposed to be called without as clause *)
 let introElimAssumsThen tac ba =
@@ -139,7 +140,7 @@ let induction_trailer abs_i abs_j bargs =
 	  let (hyps,_) =
             List.fold_left
 	      (fun (bring_ids,leave_ids) d ->
-                 let cid = get_id d in
+                 let cid = NamedDecl.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 1a45217a4..c94dcfa9d 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -60,6 +60,8 @@ open Indrec
 open Sigma.Notations
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
 let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
@@ -600,9 +602,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
   | hp :: p :: ind :: indargs ->
      let c' = 
       my_it_mkLambda_or_LetIn indargs
-        (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)
+        (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
+	  (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
+	    (mkLambda_or_LetIn (RelDecl.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]))))))
@@ -741,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind =
   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 = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
+  let ty = RelDecl.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 3e5b7b65f..fcfd26185 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -45,6 +45,8 @@ open Proofview.Notations
 open Unification
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 (* Options *)
 
 let discriminate_introduction = ref true
@@ -1662,13 +1664,13 @@ 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 d =
-  let id = get_id d in
+  let id = NamedDecl.get_id d in
   try
     let is_var id c = match kind_of_term c with
     | Var id' -> Id.equal id id'
     | _ -> false
     in
-    let c = pf_nf_evar gl (get_type d) in
+    let c = pf_nf_evar gl (NamedDecl.get_type d) in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
     if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true));
     if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false))
@@ -1686,7 +1688,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   (* The set of hypotheses using x *)
   let dephyps =
     List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
-      let id = get_id dcl in
+      let id = NamedDecl.get_id dcl in
       if not (Id.equal id hyp)
          && List.exists (fun y -> occur_var_in_decl env y dcl) deps
       then
@@ -1715,7 +1717,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 |> get_value in
+    let xval = pf_get_hyp x gl |> NamedDecl.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
       (* Find a non-recursive definition for x *)
@@ -1763,12 +1765,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let test decl =
       try
-        let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) in
+        let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.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 (get_id decl)
+            Some (NamedDecl.get_id decl)
         | _ ->
             None
       with Constr_matching.PatternMatchingFailure -> None
@@ -1782,7 +1784,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 |> get_type in
+    let c = pf_get_hyp hyp gl |> NamedDecl.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
@@ -1851,10 +1853,10 @@ let rewrite_assumption_cond cond_eq_term cl =
   let rec arec hyps gl = match hyps with
     | [] -> error "No such assumption."
     | hyp ::rest ->
-        let id = get_id hyp in
+        let id = NamedDecl.get_id hyp in
 	begin
 	  try
-            let dir = cond_eq_term (get_type hyp) gl in
+            let dir = cond_eq_term (NamedDecl.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/hints.ml b/tactics/hints.ml
index 8f3eb5eb5..a74fceb8f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -34,7 +34,8 @@ open Tacred
 open Printer
 open Vernacexpr
 open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (****************************************)
 (* General functions                    *)
@@ -782,11 +783,11 @@ let make_resolves env sigma flags pri poly ?name cr =
 
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma decl =
-  let hname = get_id decl in
+  let hname = NamedDecl.get_id decl in
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (mkVar hname, get_type decl, Univ.ContextSet.empty)]
+       (mkVar hname, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6e24cc469..36770925f 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -19,6 +19,8 @@ open Declarations
 open Tacmach.New
 open Context.Rel.Declaration
 
+module RelDecl = 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
    general disjunction, or a type with no constructors.
@@ -100,7 +102,7 @@ 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 decl -> let c = get_type decl in
+	      (fun decl -> let c = RelDecl.get_type decl in
 	                   is_local_assum decl &&
 			   isRel c &&
                            Int.equal (destRel c) mib.mind_nparams) ctx
@@ -109,7 +111,7 @@ let match_with_one_constructor style onlybinary allow_rec t =
 	  else None
 	else
 	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
-	  let cargs = List.map get_type (prod_assum ctyp) in
+	  let cargs = List.map RelDecl.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)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index bda16b01c..575710ecc 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -28,7 +28,8 @@ open Misctypes
 open Tacexpr
 open Sigma.Notations
 open Proofview.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 let var_occurs_in_pf gl id =
   let env = Proofview.Goal.env gl in
@@ -182,7 +183,7 @@ let dependent_hyps env id idlist gl =
     | [] -> []
     | d::l ->
 	(* Update the type of id1: it may have been subject to rewriting *)
-	let d = pf_get_hyp (get_id d) gl in
+	let d = pf_get_hyp (NamedDecl.get_id d) gl in
 	if occur_var_in_decl env id d
         then d :: dep_rec l
         else dep_rec l
@@ -192,7 +193,7 @@ let dependent_hyps env id idlist gl =
 let split_dep_and_nodep hyps gl =
   List.fold_right
     (fun d (l1,l2) ->
-       if var_occurs_in_pf gl (get_id d) then (d::l1,l2) else (l1,d::l2))
+       if var_occurs_in_pf gl (NamedDecl.get_id d) then (d::l1,l2) else (l1,d::l2))
     hyps ([],[])
 
 (* Computation of dids is late; must have been done in rewrite_equations*)
@@ -383,7 +384,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 get_id nodepids else [] in
+  let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in
   match othin with
     | Some thin ->
         tclTHENLIST
@@ -399,10 +400,10 @@ let rewrite_equations as_mode othin neqns names ba =
 		   tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
 	       names;
 	     tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
-               let idopt = if as_mode then Some (get_id d) else None in
+               let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
 	       intro_move idopt (if thin then MoveLast else !first_eq))
 	       nodepids;
-	     (tclMAP (fun d -> tclTRY (clear [get_id d])) depids)]
+	     (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
     | None ->
         (* simple inversion *)
         if as_mode then
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 642bf520b..1639ec54c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -29,6 +29,8 @@ open Decl_kinds
 open Proofview.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let no_inductive_inconstr env sigma constr =
   (str "Cannot recognize an inductive predicate in " ++
      pr_lconstr_env env sigma constr ++
@@ -156,7 +158,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let revargs,ownsign =
 	fold_named_context
 	  (fun env d (revargs,hyps) ->
-             let id = get_id d in
+             let id = NamedDecl.get_id d in
              if Id.List.mem id ivars then
 	       ((mkVar id)::revargs, Context.Named.add d hyps)
 	     else
@@ -206,7 +208,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ownSign = ref begin
     fold_named_context
       (fun env d sign ->
-         if mem_named_context (get_id d) global_named_context then sign
+         if mem_named_context (NamedDecl.get_id d) global_named_context then sign
 	 else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
   end in
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index 004492e78..a5ccd500c 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -13,6 +13,8 @@ open Names
 open Tacexpr
 open Context.Named.Declaration
 
+module NamedDecl = 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
     corresponding matching rule, a matching substitution to be
@@ -280,9 +282,9 @@ module PatternMatching (E:StaticEnvironment) = struct
       the name of the matched hypothesis. *)
   let hyp_match_type hypname pat hyps =
     pick hyps >>= fun decl ->
-    let id = get_id decl in
+    let id = NamedDecl.get_id decl in
     let refresh = is_local_def decl in
-    pattern_match_term refresh pat (get_type decl) () <*>
+    pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
     put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
     return id
 
@@ -319,7 +321,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 decl = Id.equal (get_id decl) matched_hyp in
+        let select_matched_hyp decl = Id.equal (NamedDecl.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 87fdcf14d..664629f34 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,7 +16,8 @@ open Declarations
 open Tacmach
 open Clenv
 open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -70,7 +71,7 @@ let nthDecl m gl =
   try List.nth (pf_hyps gl) (m-1)
   with Failure _ -> error "No such assumption."
 
-let nthHypId m gl = nthDecl m gl |> get_id
+let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
 let nthHyp m gl   = mkVar (nthHypId m gl)
 
 let lastDecl gl   = nthDecl 1 gl
@@ -81,7 +82,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 get_id (nLastDecls n gl)
+let nLastHypsId n gl = List.map NamedDecl.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
@@ -99,7 +100,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 (Id.equal id % get_id) (pf_hyps gl))
+  fst (List.split_when (Id.equal id % NamedDecl.get_id) (pf_hyps gl))
 
 (***************************************)
 (*           Clause Tacticals          *)
@@ -560,7 +561,7 @@ module New = struct
   let nthHypId m gl =
     (** We only use [id] *)
     let gl = Proofview.Goal.assume gl in
-    nthDecl m gl |> get_id
+    nthDecl m gl |> NamedDecl.get_id
   let nthHyp m gl = 
     mkVar (nthHypId m gl)
 
@@ -592,7 +593,7 @@ module New = struct
   let afterHyp id tac =
     Proofview.Goal.enter { enter = begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let rem, _ = List.split_when (Id.equal id % get_id) hyps in
+    let rem, _ = List.split_when (Id.equal id % NamedDecl.get_id) hyps in
     tac rem
     end }
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index acc0fa1ca..d8c241193 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,6 +43,10 @@ open Locusops
 open Misctypes
 open Proofview.Notations
 open Sigma.Notations
+open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 let inj_with_occurrences e = (AllOccurrences,e)
 
@@ -162,19 +166,17 @@ let _ =
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
 let unsafe_intro env store decl b =
-  let open Context.Named.Declaration in
   Refine.refine ~unsafe:true { run = begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
-    let inst = List.map (mkVar % get_id) (named_context env) in
+    let inst = List.map (mkVar % NamedDecl.get_id) (named_context env) in
     let ninst = mkRel 1 :: inst in
-    let nb = subst1 (mkVar (get_id decl)) b in
+    let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
     let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
     Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p)
   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,6 +188,7 @@ let introduction ?(check=true) id =
       errorlabstrm "Tactics.introduction"
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
+    let open Context.Named.Declaration in
     match kind_of_term (whd_evar sigma concl) with
     | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
     | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
@@ -317,7 +320,6 @@ let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
 
 (* 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) ->
@@ -339,7 +341,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 decl = Id.Set.add (get_id decl) accu in
+      let fold accu decl = Id.Set.add (NamedDecl.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
@@ -358,13 +360,13 @@ let rename_hyp repl =
       let subst = List.map make_subst repl in
       let subst c = Vars.replace_vars subst c in
       let map decl =
-        decl |> map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
-             |> map_constr subst
+        decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
+             |> NamedDecl.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 (mkVar % get_id) hyps in
+      let instance = List.map (mkVar % NamedDecl.get_id) hyps in
       Refine.refine ~unsafe:true { run = begin fun sigma ->
         Evarutil.new_evar_instance nctx sigma nconcl ~store instance
       end }
@@ -982,23 +984,21 @@ 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))
   | decl :: right ->
-    if Id.equal (get_id decl) id then
-      match right with decl::_ -> MoveBefore (get_id decl) | [] -> MoveLast
+    if Id.equal (NamedDecl.get_id decl) id then
+      match right with decl::_ -> MoveBefore (NamedDecl.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))
   | decl :: right ->
-      let hyp = get_id decl in
+      let hyp = NamedDecl.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))
@@ -1559,7 +1559,7 @@ let make_projection env sigma params cstr sign elim i n c u =
   | NotADefinedRecordUseScheme elim ->
       (* bugs: goes from right to left when i increases! *)
       let decl = List.nth cstr.cs_args i in
-      let t = get_type decl in
+      let t = RelDecl.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
@@ -1943,7 +1943,6 @@ let exact_proof c =
   end }
 
 let assumption =
-  let open Context.Named.Declaration in
   let rec arec gl only_eq = function
   | [] ->
     if only_eq then
@@ -1951,7 +1950,7 @@ let assumption =
       arec gl false hyps
     else Tacticals.New.tclZEROMSG (str "No such assumption.")
   | decl::rest ->
-    let t = get_type decl in
+    let t = NamedDecl.get_type decl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let (sigma, is_same_type) =
@@ -1962,7 +1961,7 @@ let assumption =
     in
     if is_same_type then
       (Proofview.Unsafe.tclEVARS sigma) <*>
-	Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
+	Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (NamedDecl.get_id decl)) h }
     else arec gl only_eq rest
   in
   let assumption_tac = { enter = begin fun gl ->
@@ -1992,7 +1991,7 @@ let check_is_type env sigma ty =
 
 let check_decl env sigma decl =
   let open Context.Named.Declaration in
-  let ty = get_type decl in
+  let ty = NamedDecl.get_type decl in
   let evdref = ref sigma in
   try
     let _ = Typing.e_sort_of env evdref ty in
@@ -2002,7 +2001,7 @@ let check_decl env sigma decl =
     in
     !evdref
   with e when CErrors.noncritical e ->
-    let id = get_id decl in
+    let id = NamedDecl.get_id decl in
     raise (DependsOnBody (Some id))
 
 let clear_body ids =
@@ -2034,7 +2033,7 @@ let clear_body ids =
               check_decl env sigma decl
             else sigma
           in
-          let seen = seen || List.mem_f Id.equal (get_id decl) ids in
+          let seen = seen || List.mem_f Id.equal (NamedDecl.get_id decl) ids in
           (push_named decl env, sigma, seen)
         in
         let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in
@@ -2074,13 +2073,12 @@ 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) decl ->
-      let hyp = get_id decl in
+      let hyp = NamedDecl.get_id decl in
       if Id.List.mem hyp hyps
         || List.exists (occur_var_in_decl env hyp) keep
 	|| occur_var env hyp ccl
@@ -2618,13 +2616,12 @@ 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 _ d env ->
-      let env = if Id.equal id (get_id d) then push_named_context decls env else env in
+      let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in
       push_named d env)
     ~init:(reset_context env) env
 
@@ -2763,19 +2760,18 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
   generalize_goal_gen env sigma ids i o t cl
 
 let old_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:Context.Named.Declaration.t) (toquant:Context.Named.t) =
-    if List.exists (fun d' -> occur_var_in_decl env (get_id d') d) toquant
+    if List.exists (fun d' -> occur_var_in_decl env (NamedDecl.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 get_id to_quantify_rev in
+  let qhyps = List.map NamedDecl.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
@@ -2787,7 +2783,7 @@ let old_generalize_dep ?(with_let=false) c gl =
   let body =
     if with_let then
       match kind_of_term c with
-      | Var id -> Tacmach.pf_get_hyp gl id |> get_value
+      | Var id -> Tacmach.pf_get_hyp gl id |> NamedDecl.get_value
       | _ -> None
     else None
   in
@@ -2936,7 +2932,7 @@ let unfold_body x =
   | LocalDef (_,xval,_) -> xval
   in
   Tacticals.New.afterHyp x begin fun aft ->
-  let hl = List.fold_right (fun decl cl -> (get_id decl, InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
   let rfun _ _ c = replace_vars [x, xval] c in
   let reducth h = reduct_in_hyp rfun h in
   let reductc = reduct_in_concl (rfun, DEFAULTcast) in
@@ -3255,7 +3251,6 @@ 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
@@ -3265,7 +3260,7 @@ let cook_sign hyp0_opt inhyps indvars env =
   let before = ref true in
   let maindep = ref false in
   let seek_deps env decl rhyp =
-    let hyp = get_id decl in
+    let hyp = NamedDecl.get_id decl in
     if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false)
     then begin
       before:=false;
@@ -3284,7 +3279,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 decl' -> occur_var_in_decl env (get_id decl') decl) !decldeps)
+         List.exists (fun decl' -> occur_var_in_decl env (NamedDecl.get_id decl') decl) !decldeps)
       in
       if not (List.is_empty inhyps) && Id.List.mem hyp inhyps
          || dephyp0 || depother
@@ -3307,7 +3302,7 @@ let cook_sign hyp0_opt inhyps indvars env =
   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 decl =
-    let hyp = get_id decl in
+    let hyp = NamedDecl.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
@@ -3531,13 +3526,12 @@ 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) d ->
-          let x = get_id d in
+          let x = NamedDecl.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
@@ -3567,7 +3561,6 @@ let linear vars args =
     with Seen -> false
 
 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 =
@@ -3591,7 +3584,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     let name, ty, arity =
       let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
       let decl = List.hd rel in
-      get_name decl, get_type decl, c
+      RelDecl.get_name decl, RelDecl.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
@@ -4026,14 +4019,15 @@ let is_functional_induction elimc gl =
    need a dependent one or not *)
 
 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 d -> assert (is_local_assum d); pi1 (decompose_prod_letin (get_type d))) (List.rev s.branches) in
+      let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (RelDecl.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
@@ -4095,7 +4089,6 @@ let induction_tac with_evars params indvars elim =
    induction applies with the induction hypotheses *)
 
 let apply_induction_in_context with_evars 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
@@ -4108,7 +4101,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let s = Retyping.get_sort_family_of env sigma tmpcl in
     let deps_cstr =
       List.fold_left
-        (fun a decl -> if is_local_assum decl then (mkVar (get_id decl))::a else a) [] deps in
+        (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.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
@@ -4190,7 +4183,6 @@ let induction_without_atomization isrec with_evars elim names lid =
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let open Context.Named.Declaration in
   if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
   then errorlabstrm ""
@@ -4199,7 +4191,7 @@ let clear_unselected_context id inhyps cls =
   match cls.onhyps with
   | Some hyps ->
       let to_erase d =
-        let id' = get_id d in
+        let id' = NamedDecl.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 *)
@@ -4766,7 +4758,7 @@ let interpretable_as_section_decl evd d1 d2 =
   | LocalDef _, LocalAssum _ -> false
   | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
     e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
-  | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (get_type d2)
+  | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
 
 let rec decompose len c t accu =
   let open Context.Rel.Declaration in
@@ -4779,7 +4771,6 @@ let rec decompose len c t accu =
   | _ -> assert false
 
 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 ->
@@ -4790,9 +4781,9 @@ let rec 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
+        let accu = if RelDecl.is_local_assum p
+                   then mkVar (NamedDecl.get_id decl) :: accu
+                   else accu
     in
     shrink ctx sign c t accu
 | _ -> assert false
@@ -4818,7 +4809,6 @@ 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()
@@ -4828,7 +4818,7 @@ let abstract_subproof id gk tac =
   let sign,secsign =
     List.fold_right
       (fun d (s1,s2) ->
-        let id = get_id d in
+        let id = NamedDecl.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)