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.

3 files changed, 30 insertions, 28 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index bd86f4bd27..fcb429aef4 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -18,6 +18,9 @@ open Environ
 open Evd
 open Sigma.Notations
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 let safe_evar_value sigma ev =
   try Some (Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
@@ -161,11 +164,11 @@ let is_ground_term evd t =
   not (has_undefined_evars evd t)
 
 let is_ground_env evd env =
-  let open Context.Rel.Declaration in
+  let open RelDecl in
   let is_ground_rel_decl = function
     | LocalDef (_,b,_) -> is_ground_term evd b
     | _ -> true in
-  let open Context.Named.Declaration in
+  let open NamedDecl in
   let is_ground_named_decl = function
     | LocalDef (_,b,_) -> is_ground_term evd b
     | _ -> true in
@@ -249,11 +252,10 @@ let non_instantiated sigma =
 (************************)
 
 let make_pure_subst evi args =
-  let open Context.Named.Declaration in
   snd (List.fold_right
     (fun decl (args,l) ->
       match args with
-        | a::rest -> (rest, (get_id decl, a)::l)
+        | a::rest -> (rest, (NamedDecl.get_id decl, a)::l)
         | _ -> anomaly (Pp.str "Instance does not match its signature"))
     (evar_filtered_context evi) (Array.rev_to_list args,[]))
 
@@ -327,10 +329,10 @@ let push_var id (n, s) =
 let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
   let replace_var_named_declaration id0 id decl =
-    let id' = get_id decl in
+    let id' = NamedDecl.get_id decl in
     let id' = if Id.equal id0 id' then id else id' in
     let vsubst = [id0 , mkVar id] in
-    decl |> set_id id' |> map_constr (replace_vars vsubst)
+    decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst)
   in
   let extract_if_neq id = function
     | Anonymous -> None
@@ -551,8 +553,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                     let () = Id.Map.iter check ri in
                   (* No dependency at all, we can keep this ev's context hyp *)
                     (ri, true::filter)
-                  with Depends id -> let open Context.Named.Declaration in
-                                     (Id.Map.add (get_id h) id ri, false::filter))
+                  with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
 		ctxt (Array.to_list l) (Id.Map.empty,[]) in
 	    (* Check if some rid to clear in the context of ev has dependencies
 	       in the type of ev and adjust the source of the dependency *)
@@ -591,10 +592,9 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
   let terms =
     List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids global) terms in
   let nhyps =
-    let open Context.Named.Declaration in
     let check_context decl =
-      let err = OccurHypInSimpleClause (Some (get_id decl)) in
-      map_constr (check_and_clear_in_constr env evdref err ids global) decl
+      let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in
+      NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids global) decl
     in
     let check_value vk = match force_lazy_val vk with
     | None -> vk
@@ -633,8 +633,8 @@ let process_dependent_evar q acc evm is_dependent e =
      hypotheses), they are all dependent. *)
   queue_term q true evi.evar_concl;
   List.iter begin fun decl ->
-    let open Context.Named.Declaration in
-    queue_term q true (get_type decl);
+    let open NamedDecl in
+    queue_term q true (NamedDecl.get_type decl);
     match decl with
     | LocalAssum _ -> ()
     | LocalDef (_,b,_) -> queue_term q true b
@@ -688,9 +688,8 @@ let undefined_evars_of_term evd t =
   evrec Evar.Set.empty t
 
 let undefined_evars_of_named_context evd nc =
-  let open Context.Named.Declaration in
   Context.Named.fold_outside
-    (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+    (NamedDecl.fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
     nc
     ~init:Evar.Set.empty
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 6ba8a51120..499551406b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -16,7 +16,9 @@ open Vars
 open Termops
 open Environ
 open Globnames
-open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 (** Generic filters *)
 module Filter :
@@ -226,7 +228,7 @@ let evar_instance_array test_id info args =
     if i < len then
       let c = Array.unsafe_get args i in
       if test_id d c then instrec filter ctxt (succ i)
-      else (get_id d, c) :: instrec filter ctxt (succ i)
+      else (NamedDecl.get_id d, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
@@ -235,7 +237,7 @@ let evar_instance_array test_id info args =
      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 (get_id d, c)
+        if test_id d c then None else Some (NamedDecl.get_id d, c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -243,7 +245,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 (isVarId % get_id) info args
+  evar_instance_array (isVarId % NamedDecl.get_id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -681,7 +683,7 @@ let restrict evk filter ?candidates evd =
       evar_extra = Store.empty } in
   let evar_names = EvNames.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 (mkVar % get_id) ctxt in
+  let id_inst = Array.map_of_list (mkVar % NamedDecl.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;
@@ -746,7 +748,7 @@ let evars_of_named_context nc =
   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 (get_type decl))) (get_value decl))
+      (Evar.Set.union s (evars_of_term (NamedDecl.get_type decl))) (NamedDecl.get_value decl))
     nc Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
@@ -1283,8 +1285,8 @@ let pr_meta_map mmap =
   prlist pr_meta_binding (metamap_to_list mmap)
 
 let pr_decl (decl,ok) =
-  let id = get_id decl in
-  match get_value decl with
+  let id = NamedDecl.get_id decl in
+  match NamedDecl.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 "}")
@@ -1401,9 +1403,8 @@ 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 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 pr_named_decl decl = pr_body (Name (NamedDecl.get_id decl)) (NamedDecl.get_value decl) in
+  let pr_rel_decl decl = pr_body (RelDecl.get_name decl) (RelDecl.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 638adea5d3..1497dbda80 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -24,6 +24,8 @@ open Environ
 open Termops
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 (**********************************************************************)
 (* Conventional names *)
 
@@ -295,10 +297,10 @@ let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
     (fun decl newenv ->
-       let na = named_hd newenv (get_type decl) (get_name decl) in
+       let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
-       push_rel (set_name (Name id) decl) newenv)
+       push_rel (RelDecl.set_name (Name id) decl) newenv)
     env
 
 (* 5- Looks for next fresh name outside a list; avoids also to use names that