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.

10 files changed, 56 insertions, 46 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 6a28723b8..8e6c7a70d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -32,6 +32,9 @@ open Misctypes
 open Sigma.Notations
 open Context.Named.Declaration
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (* Strictness option *)
 
 let clear ids { it = goal; sigma } =
@@ -247,7 +250,7 @@ let close_previous_case pts =
 
 let filter_hyps f gls =
   let filter_aux id =
-    let id = get_id id in
+    let id = NamedDecl.get_id id in
     if f id then
       tclIDTAC
     else
@@ -357,8 +360,7 @@ let enstack_subsubgoals env se stack gls=
 		  let nlast=succ last in
 		  let (llast,holes,metas) =
 		    meta_aux nlast (mkMeta nlast :: lenv) q in
-                    let open Context.Rel.Declaration in
-		    (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in
+		    (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in
 	    let (nlast,holes,nmetas) =
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
@@ -822,7 +824,7 @@ let define_tac id args body gls =
 let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
     | This id ->
-        Proofview.V82.of_tactic  (pf_get_hyp gls id |> set_id id |> set_type typ |> convert_hyp) gls
+        Proofview.V82.of_tactic  (pf_get_hyp gls id |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 58744b575..b34a36492 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,7 +15,8 @@ open Tacmach
 open Util
 open Declarations
 open Globnames
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
 
 let qflag=ref true
 
@@ -141,7 +142,7 @@ let build_atoms gl metagen side cciterm =
 	    end;
 	  let v = ind_hyps 0 i l gl in
 	  let g i _ decl =
-	    build_rec env polarity (lift i (get_type decl)) in
+	    build_rec env polarity (lift i (RelDecl.get_type decl)) in
 	  let f l =
 	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
@@ -152,7 +153,7 @@ let build_atoms gl metagen side cciterm =
 	  let var=mkMeta (metagen true) in
 	  let v =(ind_hyps 1 i l gl).(0) in
 	  let g i _ decl =
-	    build_rec (var::env) polarity (lift i (get_type decl)) in
+	    build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in
 	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
@@ -225,7 +226,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in
+		      let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index ffb63af07..7ffc78928 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -19,7 +19,8 @@ open Formula
 open Sequent
 open Globnames
 open Locus
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
 
@@ -36,12 +37,12 @@ let wrap n b continue seq gls=
       match nc with
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
-            let id = get_id nd in
+            let id = NamedDecl.get_id nd in
 	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in
+	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b0ffc775b..f47ab2616 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -16,6 +16,8 @@ open Libnames
 open Globnames
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 (* let msgnl = Pp.msgnl *)
 
 (*
@@ -307,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   try
 	     let witness = Int.Map.find i sub in
 	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
-	     (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun))
+	     (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -938,7 +940,7 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl decl = Nameops.out_name (get_name decl)
+let id_of_decl decl = Nameops.out_name (RelDecl.get_name decl)
 let var_of_decl decl = mkVar (id_of_decl decl)
 let revert idl =
   tclTHEN
@@ -1072,7 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	 (Name new_id)
       )
     in
-    let fresh_decl = map_name fresh_id in
+    let fresh_decl = RelDecl.map_name fresh_id in
     let princ_info : elim_scheme =
       { princ_info with
 	  params = List.map fresh_decl princ_info.params;
@@ -1119,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
+	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl)))
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl)))
+	       prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (RelDecl.get_name decl)))
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1165,7 +1167,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    let pte_to_fix,rev_info =
 	      List.fold_left_i
 		(fun i (acc_map,acc_info) decl ->
-		   let pte = get_name decl in
+		   let pte = RelDecl.get_name decl in
 		   let infos = info_array.(i) in
 		   let type_args,_ = decompose_prod infos.types in
 		   let nargs = List.length type_args in
@@ -1277,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params))
+			  (args_id@(List.map (fun decl -> Nameops.out_name (RelDecl.get_name decl)) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5e72b8672..234c3e75e 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -14,6 +14,8 @@ open Functional_principles_proofs
 open Misctypes
 open Sigma.Notations
 
+module RelDecl = Context.Rel.Declaration
+
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
 
@@ -38,7 +40,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 	| Name x ->
 	   let id = Namegen.next_ident_away x avoid in
 	   Hashtbl.add tbl id x;
-	   set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
+	   RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
 	| Anonymous -> anomaly (Pp.str "Anonymous property binder "))
   in
   let avoid = (Termops.ids_of_context env_with_params ) in
@@ -51,7 +53,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 (*   observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
   let change_predicate_sort i decl =
     let new_sort = sorts.(i) in
-    let args,_ = decompose_prod (get_type decl) in
+    let args,_ = decompose_prod (RelDecl.get_type decl) in
     let real_args =
       if princ_type_info.indarg_in_concl
       then List.tl args
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 02fe6ce3a..4d02c77c8 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -366,7 +366,6 @@ let add_pat_variables pat typ env : Environ.env =
       Context.Rel.fold_outside
 	(fun decl (env,ctxt) ->
          let open Context.Rel.Declaration in
-         (*let _,v,t = Context.Rel.Declaration.to_tuple decl in*)
 	 match decl with
 	   | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
 	   | LocalAssum (Name id, t) ->
@@ -415,8 +414,7 @@ let rec pattern_to_term_and_type env typ  = function
       in
       let constructors = Inductiveops.get_constructors env indf in
       let constructor  = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in
-      let open Context.Rel.Declaration in
-      let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in
+      let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in
       let _,cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
       let implicit_args =
@@ -615,7 +613,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
 	let new_env =
-          let open Context.Named.Declaration in
 	  match n with
 	      Anonymous -> env
 	    | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env
@@ -989,8 +986,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			      (fun acc var_as_constr arg ->
 				 if isRel var_as_constr
 				 then
-                                   let open Context.Rel.Declaration in
-				   let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in
+				   let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in
 				   match na with
 				     | Anonymous -> acc
 				     | Name id' ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 18817f504..51cf7f4f4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,4 +1,3 @@
-open Context.Rel.Declaration
 open CErrors
 open Util
 open Names
@@ -13,11 +12,13 @@ open Misctypes
 open Decl_kinds
 open Sigma.Notations
 
+module RelDecl = Context.Rel.Declaration
+
 let is_rec_info scheme_info =
   let test_branche min acc decl =
     acc || (
       let new_branche =
-	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in
+	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in
       let free_rels_in_br = Termops.free_rels new_branche in
       let max = min + scheme_info.Tactics.npredicates in
       Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 26fc88a60..0178c44d0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,6 +23,8 @@ open Misctypes
 open Termops
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 (* Some pretty printing function for debugging purpose *)
 
 let pr_binding prc  =
@@ -137,7 +139,7 @@ let generate_type evd g_to_f f graph i =
   let fun_ctxt,res_type =
     match ctxt with
       | [] | [_] -> anomaly (Pp.str "Not a valid context")
-      | decl :: fun_ctxt -> fun_ctxt, get_type decl
+      | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
   in
   let rec args_from_decl i accu = function
   | [] -> accu
@@ -148,7 +150,7 @@ let generate_type evd g_to_f f graph i =
     args_from_decl (succ i) (t :: accu) l
   in
   (*i We need to name the vars [res] and [fv] i*)
-  let filter = fun decl -> match get_name decl with
+  let filter = fun decl -> match RelDecl.get_name decl with
 			   | Name id -> Some id
 			   | Anonymous -> None
   in
@@ -269,7 +271,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	(fun decl ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl)))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl)))))
 	)
 	branches
     in
@@ -399,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     | hres::res::decl::ctxt ->
 		let res = Termops.it_mkLambda_or_LetIn
 			    (Termops.it_mkProd_or_LetIn concl [hres;res])
-			    (LocalAssum (get_name decl, get_type decl) :: ctxt)
+			    (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
 		in
 		res
 	)
@@ -415,7 +417,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
 	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -425,7 +427,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
 	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
@@ -682,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(fun decl ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl)))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl)))
 	)
 	branches
     in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index de4210af5..d9933cf41 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -26,6 +26,8 @@ open Glob_termops
 open Decl_kinds
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+
 (** {1 Utilities}  *)
 
 (** {2 Useful operations on constr and glob_constr} *)
@@ -137,7 +139,7 @@ let showind (id:Id.t) =
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
   List.iter (fun decl ->
     print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
-    prconstr (get_type decl); print_string "\n")
+    prconstr (RelDecl.get_type decl); print_string "\n")
     ib1.mind_arity_ctxt;
     Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1);
   Array.iteri
@@ -460,12 +462,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
   let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
   let _ = prstr "\notherprms1:\n" in
   let _ =
-    List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : ");
-			   prconstr (get_type decl); prstr "\n")
+    List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : ");
+			   prconstr (RelDecl.get_type decl); prstr "\n")
     otherprms1 in
   let _ = prstr "\notherprms2:\n" in
   let _ =
-    List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n")
+    List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n")
     otherprms2 in
   {
     ident=id;
@@ -827,7 +829,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     List.fold_left
       (fun (acc,env) decl ->
         let nm = Context.Rel.Declaration.get_name decl in
-        let c = get_type decl in
+        let c = RelDecl.get_type decl in
         let typ = Constrextern.extern_constr false env Evd.empty c in
         let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
         CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c5c44ef20..1afc6500b 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -30,6 +30,7 @@ open Misctypes
 open Proofview.Notations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
@@ -1697,8 +1698,8 @@ let destructure_hyps =
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
       | decl::lit ->
-          let i = get_id decl in
-	  begin try match destructurate_prop (get_type decl) with
+          let i = NamedDecl.get_id decl in
+	  begin try match destructurate_prop (NamedDecl.get_type decl) with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
@@ -1808,13 +1809,13 @@ let destructure_hyps =
 		    match destructurate_type (pf_nf typ) with
 		    | Kapp(Nat,_) ->
                         (Tacticals.New.tclTHEN
-			   (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
-                                                           decl))
+			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+                                                                     decl))
 			   (loop lit))
 		    | Kapp(Z,_) ->
                         (Tacticals.New.tclTHEN
-			   (convert_hyp_no_check (set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
-                                                           decl))
+			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+                                                                     decl))
 			   (loop lit))
 		    | _ -> loop lit
                   end