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.

7 files changed, 41 insertions, 29 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 111a947a9..75f56c6b9 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -10,7 +10,8 @@ open Util
 open Pp
 open Term
 open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -77,7 +78,7 @@ module V82 = struct
     let evars = Sigma.to_evar_map evars in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (mkVar % get_id) ctxt in
+    let inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
     (evk, ev, evars)
 
@@ -148,7 +149,7 @@ module V82 = struct
     let env = env sigma gl in
     let genv = Global.env () in
     let is_proof_var decl =
-      try ignore (Environ.lookup_named (get_id decl) genv); false
+      try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 39dff4aca..19f5f5d3f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -24,6 +24,8 @@ open Retyping
 open Misctypes
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 type refiner_error =
 
   (* Errors raised by the refiner *)
@@ -162,7 +164,7 @@ let reorder_context env sign ord =
           (match ctxt_head with
             | [] -> error_no_such_hypothesis (List.hd ord)
             | d :: ctxt ->
-                let x = get_id d in
+                let x = NamedDecl.get_id d in
                 if Id.Set.mem x expected then
                   step ord (Id.Set.remove x expected)
                     ctxt (push_item x d moved_hyps) ctxt_tail
@@ -178,7 +180,7 @@ let reorder_val_context env sign ord =
 
 
 let check_decl_position env sign d =
-  let x = get_id d in
+  let x = NamedDecl.get_id d in
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
@@ -204,8 +206,8 @@ let move_location_eq m1 m2 = match m1, m2 with
 let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
   | d :: right ->
-      if Id.equal (get_id d) h then
-	match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst
+      if Id.equal (NamedDecl.get_id d) h then
+	match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst
       else
        get_hyp_after h right
 
@@ -213,7 +215,7 @@ let split_sign hfrom hto l =
   let rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
     | d :: right ->
-        let hyp = get_id d in
+        let hyp = NamedDecl.get_id d in
       	if Id.equal hyp hfrom then
 	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
@@ -235,24 +237,24 @@ let move_hyp toleft (left,declfrom,right) hto =
   let env = Global.env() in
   let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env (get_id d2) d
-    else occur_var_in_decl env (get_id d) d2
+    then occur_var_in_decl env (NamedDecl.get_id d2) d
+    else occur_var_in_decl env (NamedDecl.get_id d) d2
   in
   let rec moverec first middle = function
     | [] ->
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
 	  error_no_such_hypothesis (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
-    | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) ->
+    | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
 	List.rev first @ List.rev middle @ right
     | d :: right ->
-        let hyp = get_id d in
+        let hyp = NamedDecl.get_id d in
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
+	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
@@ -489,16 +491,16 @@ and mk_casegoals sigma goal goalacc p c =
 
 
 let convert_hyp check sign sigma d =
-  let id = get_id d in
-  let b = get_value d in
+  let id = NamedDecl.get_id d in
+  let b = NamedDecl.get_value d in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
     apply_to_hyp check sign id
       (fun _ d' _ ->
-        let c = get_value d' in
+        let c = NamedDecl.get_value d' in
         let env = Global.env_of_context sign in
-        if check && not (is_conv env sigma (get_type d) (get_type d')) then
+        if check && not (is_conv env sigma (NamedDecl.get_type d) (NamedDecl.get_type d')) then
 	  errorlabstrm "Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7605f6387..4cb9f03ce 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -18,6 +18,8 @@ open Util
 open Pp
 open Names
 
+module NamedDecl = Context.Named.Declaration
+
 (*** Proof Modes ***)
 
 (* Type of proof modes :
@@ -276,7 +278,7 @@ let set_used_variables l =
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
   let ctx_set =
-    List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
   let aux env entry (ctx, all_safe, to_clear as orig) =
     match entry with
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 5b24a1fb2..a125fb10d 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -12,6 +12,8 @@ open Util
 open Vernacexpr
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let to_string e =
   let rec aux = function
     | SsEmpty -> "()"
@@ -39,10 +41,10 @@ let rec close_fwd e s =
                | LocalAssum _ -> Id.Set.empty
                | LocalDef (_,b,_) -> global_vars_set e b
       in
-      let vty = global_vars_set e (get_type decl) in
+      let vty = global_vars_set e (NamedDecl.get_type decl) in
       let vbty = Id.Set.union vb vty in
       if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
-      then Id.Set.add (get_id decl) (Id.Set.union s vbty) else s)
+      then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s)
     s (named_context e)
     in
   if Id.Set.equal s s' then s else close_fwd e s'
@@ -65,13 +67,13 @@ and set_of_id env ty id =
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
   else if Id.to_string id = "All" then
-    List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
+    List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
   else if CList.mem_assoc_f Id.equal id !known_names then
     process_expr env (CList.assoc_f Id.equal id !known_names) []
   else Id.Set.singleton id
 
 and full_set env =
-  List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
+  List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
   let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 76e2d7dc5..139862b8f 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -11,6 +11,8 @@ open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let extract_prefix env info =
   let ctx1 = List.rev (Environ.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
@@ -26,7 +28,7 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = get_type decl in
+    let t = NamedDecl.get_type decl in
     let evdref = ref sigma in
     let _ = Typing.e_sort_of env evdref t in
     let () = match decl with
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ebd30820b..d9ab2fbdb 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -13,7 +13,8 @@ open Evd
 open Environ
 open Proof_type
 open Logic
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 let sig_it x = x.it
 let project x = x.sigma
@@ -202,7 +203,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   let { it = gls; sigma = sigma; } = rslt in
   let hyps:Context.Named.t list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
-  let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in
+  let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
   let newhyps =
     List.map
       (fun hypl -> List.subtract cmp hypl oldhyps)
@@ -215,7 +216,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
+	   (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
   Feedback.msg_notice
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 50984c48e..957843bc9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -21,6 +21,8 @@ open Refiner
 open Sigma.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 let re_sig it  gc = { it = it; sigma = gc; }
 
 (**************************************************************)
@@ -46,7 +48,7 @@ let pf_hyps_types gls  =
                    | LocalDef (id,_,x) -> id, x)
            sign
 
-let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id
+let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
@@ -57,7 +59,7 @@ let pf_get_hyp gls id =
     raise (RefinerError (NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  pf_get_hyp gls id |> get_type
+  pf_get_hyp gls id |> NamedDecl.get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -199,7 +201,7 @@ module New = struct
     sign
 
   let pf_get_hyp_typ id gl =
-    pf_get_hyp id gl |> get_type
+    pf_get_hyp id gl |> NamedDecl.get_type
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in