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

3 files changed, 16 insertions, 16 deletions

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)