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.

9 files changed, 64 insertions, 51 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 30b7f299f8..9a7ea3cde9 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -25,6 +25,8 @@ open Globnames
 open Printer
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 (** For a constant c in a module sealed by an interface (M:T and
     not M<:T), [Global.lookup_constant] may return a [constant_body]
     without body. We fix this by looking in the implementation
@@ -144,7 +146,7 @@ let label_of = function
 
 let rec traverse current ctx accu t = match kind_of_term t with
 | Var id ->
-  let body () = Global.lookup_named id |> get_value in
+  let body () = Global.lookup_named id |> NamedDecl.get_value in
   traverse_object accu body (VarRef id)
 | Const (kn, _) ->
   let body () = Global.body_of_constant_body (lookup_constant kn) in
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 180b836ea5..81e17ffb59 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -25,7 +25,8 @@ open Tactics
 open Ind_tables
 open Misctypes
 open Proofview.Notations
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
 
 let out_punivs = Univ.out_punivs
 
@@ -150,14 +151,14 @@ let build_beq_scheme mode kn =
           ( fun a b decl -> (* mkLambda(n,b,a) ) *)
                 (* here I leave the Naming thingy so that the type of
                   the function is more readable for the user *)
-                mkNamedLambda (eqName (get_name decl)) b a )
+                mkNamedLambda (eqName (RelDecl.get_name decl)) b a )
                 c (List.rev eqs_typ) lnamesparrec
        in
         List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *)
           (* Same here , hoping the auto renaming will do something good ;)  *)
           mkNamedLambda
-                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
-                (get_type decl)  a) eq_input lnamesparrec
+                (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (RelDecl.get_type decl)  a) eq_input lnamesparrec
  in
  let make_one_eq cur =
   let u = Univ.Instance.empty in
@@ -249,7 +250,7 @@ let build_beq_scheme mode kn =
                     | 0 -> Lazy.force tt
                     | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
                       for ndx = 0 to nb_cstr_args-1 do
-                        let cc = get_type (List.nth constrsi.(i).cs_args ndx) in
+                        let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
                           let eqA, eff' = compute_A_equality rel_list
                                           nparrec
                                           (nparrec+3+2*nb_cstr_args)
@@ -268,14 +269,14 @@ let build_beq_scheme mode kn =
                           (Array.sub eqs 1 (nb_cstr_args - 1))
                   )
    		  in
-		    (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a)) cc
+		    (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) cc
                     (constrsj.(j).cs_args)
 		)
 	      else ar2.(j) <- (List.fold_left (fun a decl ->
-			mkLambda (get_name decl, get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
+			mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
 	    done;
 
-	  ar.(i) <- (List.fold_left (fun a decl -> mkLambda (get_name decl, get_type decl, a))
+	  ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a))
 			(mkCase (ci,do_predicate rel_list nb_cstr_args,
 				  mkVar (Id.of_string "Y") ,ar2))
 			 (constrsi.(i).cs_args))
@@ -489,7 +490,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al  )]
 *)
 let list_id l = List.fold_left ( fun a decl -> let s' =
-      match get_name decl with
+      match RelDecl.get_name decl with
         Name s -> Id.to_string s
       | Anonymous -> "A" in
           (Id.of_string s',Id.of_string ("eq_"^s'),
@@ -537,8 +538,8 @@ let compute_bl_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a decl -> mkNamedProd
-                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
-                (get_type decl) a) eq_input lnamesparrec
+                (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -680,8 +681,8 @@ let compute_lb_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) lb_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a decl -> mkNamedProd
-                (match (get_name decl) with Name s -> s | Anonymous ->  Id.of_string "A")
-                (get_type decl)  a) eq_input lnamesparrec
+                (match (RelDecl.get_name decl) with Name s -> s | Anonymous ->  Id.of_string "A")
+                (RelDecl.get_type decl)  a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
@@ -821,8 +822,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a decl -> mkNamedProd
-                (match get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
-                (get_type decl) a) eq_input lnamesparrec
+                (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
       let n = Id.of_string "x" and
           m = Id.of_string "y" in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d6a6162f9f..a6fb48749c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -22,6 +22,8 @@ open Constrintern
 open Constrexpr
 open Sigma.Notations
 open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
 (*i*)
 
 open Decl_kinds
@@ -77,13 +79,13 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 let type_ctx_instance evars env ctx inst subst =
   let rec aux (subst, instctx) l = function
     decl :: ctx ->
-      let t' = substl subst (get_type decl) in
+      let t' = substl subst (RelDecl.get_type decl) in
       let c', l =
 	match decl with
 	| LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
 	| LocalDef (_,b,_) -> substl subst b, l
       in
-      let d = get_name decl, Some c', t' in
+      let d = RelDecl.get_name decl, Some c', t' in
 	aux (c' :: subst, d :: instctx) l ctx
     | [] -> subst
   in aux (subst, []) inst (List.rev ctx)
@@ -156,7 +158,6 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     let cl, u = Typeclasses.typeclass_univ_instance k in
     let _, args = 
       List.fold_right (fun decl (args, args') ->
-        let open Context.Rel.Declaration in
 	match decl with
 	| LocalAssum _ -> (List.tl args, List.hd args :: args')
 	| LocalDef (_,b,_) -> (args, substl args' b :: args'))
@@ -229,7 +230,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		(fun (props, rest) decl ->
 		  if is_local_assum decl then
 		    try
-		      let is_id (id', _) = match get_name decl, get_id id' with
+		      let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
 			| Name id, (_, id') -> Id.equal id id'
 			| Anonymous, _ -> false
                       in
@@ -347,7 +348,7 @@ let named_of_rel_context l =
   let acc, ctx =
     List.fold_right
       (fun decl (subst, ctx) ->
-        let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+        let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
 	let d = match decl with
 	  | LocalAssum (_,t) -> id, None, substl subst t
 	  | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 097865648e..7274ac1701 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -39,6 +39,8 @@ open Sigma.Notations
 open Context.Rel.Declaration
 open Entries
 
+module RelDecl = Context.Rel.Declaration
+
 let do_universe poly l = Declare.do_universe poly l
 let do_constraint poly l = Declare.do_constraint poly l
 
@@ -457,7 +459,7 @@ let sign_level env evd sign =
       | LocalDef _ -> lev, push_rel d env
       | LocalAssum _ ->
 	let s = destSort (Reduction.whd_all env 
-			    (nf_evar evd (Retyping.get_type_of env evd (get_type d))))
+			    (nf_evar evd (Retyping.get_type_of env evd (RelDecl.get_type d))))
 	in
 	let u = univ_of_sort s in
 	  (Univ.sup u lev, push_rel d env))
@@ -576,7 +578,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (fun decl -> out_name (get_name decl)) assums in
+  let params = List.map (fun decl -> out_name (RelDecl.get_name decl)) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in
@@ -909,8 +911,8 @@ let rec telescope = function
       let ty, tys, (k, constr) =
 	List.fold_left
 	  (fun (ty, tys, (k, constr)) decl ->
-            let t = get_type decl in
-            let pred = mkLambda (get_name decl, t, ty) in
+            let t = RelDecl.get_type decl in
+            let pred = mkLambda (RelDecl.get_name decl, t, ty) in
 	    let ty = Universes.constr_of_global (Lazy.force sigT).typ in
 	    let intro = Universes.constr_of_global (Lazy.force sigT).intro in
 	    let sigty = mkApp (ty, [|t; pred|]) in
@@ -920,7 +922,7 @@ let rec telescope = function
       in
       let (last, subst) = List.fold_right2
         (fun pred decl (prev, subst) ->
-          let t = get_type decl in
+          let t = RelDecl.get_type decl in
 	  let p1 = Universes.constr_of_global (Lazy.force sigT).proj1 in
 	  let p2 = Universes.constr_of_global (Lazy.force sigT).proj2 in
 	  let proj1 = applistc p1 [t; pred; prev] in
@@ -1133,7 +1135,7 @@ let interp_recursive isfix fixl notations =
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
-  let fixctxnames = List.map (fun (_,ctx) -> List.map get_name ctx) fixctxs in
+  let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in
 
   (* Build the fix declaration block *)
   (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ff4c18ad21..d2deb9e1eb 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -25,6 +25,8 @@ open Printer
 open Evd
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 (* This simplifies the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
@@ -35,9 +37,9 @@ let contract env lc =
           l := (Vars.substl !l c') :: !l;
           env
       | _ ->
-          let t' = Vars.substl !l (get_type decl) in
-          let c' = Option.map (Vars.substl !l) (get_value decl) in
-          let na' = named_hd env t' (get_name decl) in
+          let t' = Vars.substl !l (RelDecl.get_type decl) in
+          let c' = Option.map (Vars.substl !l) (RelDecl.get_value decl) in
+          let na' = named_hd env t' (RelDecl.get_name decl) in
           l := (mkRel 1) :: List.map (Vars.lift 1) !l;
           match c' with
           | None -> push_rel (LocalAssum (na',t')) env
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 29d7457321..b3c1623e07 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -20,6 +20,8 @@ open Pp
 open CErrors
 open Util
 
+module NamedDecl = Context.Named.Declaration
+
 let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
@@ -51,7 +53,6 @@ type oblinfo =
   where n binders were passed through. *)
 
 let subst_evar_constr evs n idf t =
-  let open Context.Named.Declaration in
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
@@ -74,6 +75,7 @@ let subst_evar_constr evs n idf t =
 	in
 	let args =
 	  let rec aux hyps args acc =
+             let open Context.Named.Declaration in
 	     match hyps, args with
 		 (LocalAssum _ :: tlh), (c :: tla) ->
 		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
@@ -116,9 +118,9 @@ let etype_of_evar evs hyps concl =
   let open Context.Named.Declaration in
   let rec aux acc n = function
       decl :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar (get_type decl) in
+	let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
 	let t'' = subst_vars acc 0 t' in
-	let rest, s', trans' = aux (get_id decl :: acc) (succ n) tl in
+	let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
 	let trans' = Id.Set.union trans trans' in
 	  (match decl with
@@ -598,7 +600,6 @@ let decompose_lam_prod c ty =
   in aux Context.Rel.empty c ty
 
 let shrink_body c ty =
-  let open Context.Rel.Declaration in
   let ctx, b, ty =
     match ty with
     | None ->
@@ -613,6 +614,7 @@ let shrink_body c ty =
         if noccurn 1 b && Option.cata (noccurn 1) true ty then
 	  subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
 	else
+          let open Context.Rel.Declaration in
 	  let args = if is_local_assum decl then mkRel i :: args else args in
           mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
 	  succ i, args)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 71d070776d..9d14bdf4c8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -27,6 +27,8 @@ open Goptions
 open Sigma.Notations
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 (********** definition d'un record (structure) **************)
 
 (** Flag governing use of primitive projections. Disabled by default. *)
@@ -82,7 +84,7 @@ let compute_constructor_level evars env l =
   List.fold_right (fun d (env, univ) ->
     let univ = 
       if is_local_assum d then
-	let s = Retyping.get_sort_of env evars (get_type d) in
+	let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
 	  Univ.sup (univ_of_sort s) univ 
       else univ
     in (push_rel d env, univ)) 
@@ -167,7 +169,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
 
 let degenerate_decl decl =
-  let id = match get_name decl with
+  let id = match RelDecl.get_name decl with
     | Name id -> id
     | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
   match decl with
@@ -288,8 +290,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
       (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
-        let fi = get_name decl in
-        let ti = get_type decl in
+        let fi = RelDecl.get_name decl in
+        let ti = RelDecl.get_type decl in
 	let (sp_projs,i,subst) =
 	  match fi with
 	  | Anonymous ->
@@ -362,17 +364,17 @@ let structure_signature ctx =
       | [decl] ->
         let env = Environ.empty_named_context_val in
         let evm = Sigma.Unsafe.of_evar_map evm in
-        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
+        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in
         let evm = Sigma.to_evar_map evm in
         evm
       | decl::tl ->
           let env = Environ.empty_named_context_val in
           let evm = Sigma.Unsafe.of_evar_map evm in
-          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
+          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in
           let evm = Sigma.to_evar_map evm in
 	  let new_tl = Util.List.map_i
 	    (fun pos decl ->
-	       map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
+	       RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
 	  deps_to_evar evm new_tl in
   deps_to_evar Evd.empty (List.rev ctx)
 
@@ -422,7 +424,7 @@ let implicits_of_context ctx =
       | Name n -> Some n
       | Anonymous -> None
     in ExplByPos (i, explname), (true, true, true))
-    1 (List.rev (Anonymous :: (List.map get_name ctx)))
+    1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
 let declare_class finite def poly ctx id idbuild paramimpls params arity 
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
@@ -476,13 +478,13 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
 			      if b then Backward, pri else Forward, pri) coe)
 	  coers priorities
        in
-       let l = List.map3 (fun decl b y -> get_name decl, b, y)
+       let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
          (List.rev fields) coers (Recordops.lookup_projections ind)
        in IndRef ind, l
   in
   let ctx_context =
     List.map (fun decl ->
-      match Typeclasses.class_of_constr (get_type decl) with
+      match Typeclasses.class_of_constr (RelDecl.get_type decl) with
       | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
       | None -> None)
       params, params
diff --git a/toplevel/search.ml b/toplevel/search.ml
index e670b59b79..d1c108c375 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -20,6 +20,8 @@ open Globnames
 open Nametab
 open Goptions
 
+module NamedDecl = Context.Named.Declaration
+
 type filter_function = global_reference -> env -> constr -> bool
 type display_function = global_reference -> env -> constr -> unit
 
@@ -68,8 +70,7 @@ let iter_constructors indsp u fn env nconstr =
   done
 
 let iter_named_context_name_type f =
-  let open Context.Named.Declaration in
-  List.iter (fun decl -> f (get_id decl) (get_type decl))
+  List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl))
 
 (* General search over hypothesis of a goal *)
 let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
@@ -81,13 +82,12 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
 
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
-  let open Context.Named.Declaration in
   let env = Global.env () in
   let iter_obj (sp, kn) lobj = match object_tag lobj with
   | "VARIABLE" ->
     begin try
       let decl = Global.lookup_named (basename sp) in
-      fn (VarRef (get_id decl)) env (get_type decl)
+      fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
     with Not_found -> (* we are in a section *) () end
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f69c4fa186..5b746ca46b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -33,6 +33,8 @@ open Misctypes
 open Locality
 open Sigma.Notations
 
+module NamedDecl = Context.Named.Declaration
+
 (** TODO: make this function independent of Ltac *)
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
@@ -848,14 +850,13 @@ let vernac_set_end_tac tac =
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables e =
-  let open Context.Named.Declaration in
   let env = Global.env () in
   let tys =
     List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
   List.iter (fun id -> 
-    if not (List.exists (Id.equal id % get_id) vars) then
+    if not (List.exists (Id.equal id % NamedDecl.get_id) vars) then
       errorlabstrm "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
@@ -1507,7 +1508,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl()
+    v 0 (pr_id id ++ str":" ++ pr_constr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
     | NoHyp | Not_found -> print_about ref_or_by_not