Standardisation of function names about global references (especially, renaming of constr_of_reference into constr_of_global)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 21 insertions, 21 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 799867675f..3ac3b42f43 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -200,7 +200,7 @@ let refute_tac axioms disaxioms id p gls =
   let tt1=make_term t1 and tt2=make_term t2 in
   let intype=pf_type_of gls tt1 in
   let neweq=
-    mkApp(constr_of_reference Coqlib.glob_eq,
+    mkApp(constr_of_global Coqlib.glob_eq,
 	  [|intype;tt1;tt2|]) in
   let hid=pf_get_new_id (id_of_string "Heq") gls in
   let false_t=mkApp (mkVar id,[|mkVar hid|]) in
@@ -225,7 +225,7 @@ let discriminate_tac axioms cstr p gls =
 		  [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
   let endt=mkApp (Lazy.force eq_rect_theo,
 		  [|outtype;trivial;pred;identity;concl;injt|]) in
-  let neweq=mkApp(constr_of_reference Coqlib.glob_eq,[|intype;tt1;tt2|]) in
+  let neweq=mkApp(constr_of_global Coqlib.glob_eq,[|intype;tt1;tt2|]) in
     tclTHENS (true_cut (Name hid) neweq) 
       [proof_tac axioms p;exact_check endt] gls
       
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 32264a0041..0eb35e95b1 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -385,7 +385,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  List.iter 
 	    (option_iter 
 	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
-	    (find_structure ip).s_PROJ 
+	    (lookup_structure ip).s_PROJ 
 	with Not_found -> ()
 	end; 
 	Record field_glob
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 53ab0a6d9c..7dc01a461e 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -108,7 +108,7 @@ let mk_open_instance id gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl (constr_of_reference id) in
+      let typ=pf_type_of gl (constr_of_global id) in
 	(* since we know we will get a product, 
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -144,7 +144,7 @@ let left_instance_tac (inst,id) continue seq=
 	    [tclTHENLIST
 	       [introf;
 		(fun gls->generalize 
-		   [mkApp(constr_of_reference id,
+		   [mkApp(constr_of_global id,
 			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
 		introf;
 		tclSOLVE [wrap 1 false continue 
@@ -160,10 +160,10 @@ let left_instance_tac (inst,id) continue seq=
 		let (rc,ot)= mk_open_instance id gl m t in
 		let gt= 
 		  it_mkLambda_or_LetIn 
-		    (mkApp(constr_of_reference id,[|ot|])) rc in
+		    (mkApp(constr_of_global id,[|ot|])) rc in
 		  generalize [gt] gl
 	    else
-	      generalize [mkApp(constr_of_reference id,[|t|])]
+	      generalize [mkApp(constr_of_global id,[|t|])]
 	  in
 	    tclTHENLIST 
 	      [special_generalize;
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 3474fe00c3..1b96eb98ce 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -57,15 +57,15 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq=
-  try exact_no_check (constr_of_reference (find_left t seq)) 
+  try exact_no_check (constr_of_global (find_left t seq)) 
   with Not_found->tclFAIL 0 "No axiom link" 
 
 let ll_atom_tac a backtrack id continue seq= 
   tclIFTHENELSE
     (try 
       tclTHENLIST
-	[generalize [mkApp(constr_of_reference id,
-			   [|constr_of_reference (find_left a seq)|])];
+	[generalize [mkApp(constr_of_global id,
+			   [|constr_of_global (find_left a seq)|])];
 	 clear_global id;
 	 intro]
     with Not_found->tclFAIL 0 "No link") 
@@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in  
    tclIFTHENELSE
      (tclTHENLIST 
-      [simplest_elim (constr_of_reference id);
+      [simplest_elim (constr_of_global id);
        clear_global id; 
        tclDO n intro])
      (wrap n false continue seq)
@@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n intro;
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (simplest_elim (constr_of_reference id))
+      (simplest_elim (constr_of_global id))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  simplest_elim (constr_of_reference id)
+  simplest_elim (constr_of_global id)
 
 (* left arrow connective rules *)
 
@@ -127,7 +127,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
-       let head=mkApp ((lift p (constr_of_reference id)),[|capply|]) in
+       let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
 	 Sign.it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
        let newhyps=list_tabulate myterm lp in
@@ -141,7 +141,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
 let ll_arrow_tac a b c backtrack id continue seq=
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
   let d=mkLambda (Anonymous,b,
-		  mkApp ((constr_of_reference id),
+		  mkApp ((constr_of_global id),
 			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
       (tclTHENS (cut c)
@@ -150,7 +150,7 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	     clear_global id;
 	     wrap 1 false continue seq];
 	  tclTHENS (cut cc) 
-            [exact_no_check (constr_of_reference id); 
+            [exact_no_check (constr_of_global id); 
 	     tclTHENLIST 
 	       [generalize [d];
 		clear_global id;
@@ -175,7 +175,7 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in  
     tclIFTHENELSE
-      (simplest_elim (constr_of_reference id))
+      (simplest_elim (constr_of_global id))
       (tclTHENLIST [clear_global id;
                     tclDO n intro;
                     (wrap (n-1) false continue seq)]) 
@@ -189,7 +189,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	  [intro;
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
-	      let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
+	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
 		tclTHEN (generalize [term]) (clear [id0]) gls);  
 	   clear_global id;
 	   intro;
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 8c2c9a3da1..90defda9c6 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -255,7 +255,7 @@ let empty_seq depth=
 
 let create_with_ref_list l depth gl=
   let f gr seq=
-    let c=constr_of_reference gr in    
+    let c=constr_of_global gr in    
     let typ=(pf_type_of gl c) in
       add_formula Hyp gr typ seq gl in
     List.fold_right f l (empty_seq depth)
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index e0f88ba69a..ef9f1280bc 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -40,7 +40,7 @@ let get_hyp_by_name g name =
 (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
    Loïc *)
   with _ -> (let c = Nametab.global (Ident (zz,name)) in
-             ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c)))
+             ("cste",type_of (Global.env()) Evd.empty (constr_of_global c)))
 ;;
 
 type pbp_atom =
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index 54229a9bc8..ad7b5a0534 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -235,7 +235,7 @@ let coq_do_omega = lazy (constant  "do_omega")
 (**
 let constant dir s =
    try
-     Libnames.constr_of_reference 
+     Libnames.constr_of_global 
        (Nametab.absolute_reference
 	  (Libnames.make_path
              (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))