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

16 files changed, 39 insertions, 39 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)))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index dd9ddb16da..3a9dc3a75a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1198,7 +1198,7 @@ let is_global id =
     false
 
 let global_reference id = 
-  constr_of_reference (locate_reference (make_short_qualid id))
+  constr_of_global (locate_reference (make_short_qualid id))
 
 let construct_reference ctx id =
   try
@@ -1207,5 +1207,5 @@ let construct_reference ctx id =
     global_reference id
 
 let global_reference_in_absolute_module dir id = 
-  constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id))
+  constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index fa939d0aab..3a0a5047bf 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -31,7 +31,7 @@ let gen_reference locstr dir s =
     anomaly (locstr^": cannot find "^(string_of_path sp))
     
 let gen_constant locstr dir s = 
-  constr_of_reference (gen_reference locstr dir s)
+  constr_of_global (gen_reference locstr dir s)
 
 let list_try_find f = 
   let rec try_find_f = function
@@ -50,7 +50,7 @@ let gen_constant_in_modules locstr dirs s =
   let all = Nametab.locate_all (make_short_qualid id) in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
-    | [x] -> constr_of_reference x
+    | [x] -> constr_of_global x
     | [] ->
 	anomalylabstrm "" (str (locstr^": cannot find "^s^
 	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
diff --git a/parsing/search.ml b/parsing/search.ml
index 8435f4b4bb..da57d90023 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -54,7 +54,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	(try 
 	   let (idc,_,typ) = get_variable (basename sp) in 
            if refopt = None
-	     || head_const typ = constr_of_reference (out_some refopt)
+	     || head_const typ = constr_of_global (out_some refopt)
 	   then
 	     fn (VarRef idc) env typ
 	 with Not_found -> (* we are in a section *) ())
@@ -62,7 +62,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	let kn = locate_constant (qualid_of_sp sp) in
 	let {const_type=typ} = Global.lookup_constant kn in
         if refopt = None
-	  || head_const typ = constr_of_reference (out_some refopt)
+	  || head_const typ = constr_of_global (out_some refopt)
 	then
 	  fn (ConstRef kn) env typ
     | "INDUCTIVE" -> 
@@ -210,7 +210,7 @@ type glob_search_about_item =
   | GlobSearchString of string
 
 let search_about_item (itemref,typ) = function
-  | GlobSearchRef ref -> Termops.occur_term (constr_of_reference ref) typ
+  | GlobSearchRef ref -> Termops.occur_term (constr_of_global ref) typ
   | GlobSearchString s -> string_string_contains (name_of_reference itemref) s
 
 let raw_search_about filter_modules display_function l =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index dc6df2c92f..5f6f1522f5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -100,11 +100,11 @@ let apprec_nohdbeta env isevars c =
      (t2 us2) = (cstr us)
      extra_args1 = extra_args2
 
-   by finding a record R and an object c := [xs:bs](Build_R a1..am v1..vn)
+   by finding a record R and an object c := [xs:bs](Build_R params v1..vn)
    with vi = (cstr us), for which we know that the i-th projection proji
    satisfies
 
-      (proji params c) = (cstr us)
+      (proji params (c xs)) = (cstr us)
 
    Rem: such objects, usable for conversion, are defined in the objdef
    table; practically, it amounts to "canonically" equip t2 into a
@@ -116,7 +116,7 @@ let check_conv_record (t1,l1) (t2,l2) =
     let proji = reference_of_constr t1 in
     let cstr = reference_of_constr t2 in
     let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
-      canonical_structure_info (proji, cstr) in
+      lookup_canonical_conversion (proji, cstr) in
     let params1, c1, extra_args1 =
       match list_chop (List.length params) l1 with 
 	| params1, c1::extra_args1 -> params1, c1, extra_args1
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 60c9321add..e6d674a5e0 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -521,11 +521,11 @@ let lookup_eliminator ind_sp s =
   let ref = ConstRef (make_con mp dp (label_of_id id)) in
   try 
     let _ = sp_of_global ref in
-    constr_of_reference ref
+    constr_of_global ref
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-  try constr_of_reference (Nametab.locate (make_short_qualid id))
+  try constr_of_global (Nametab.locate (make_short_qualid id))
   with Not_found ->
     errorlabstrm "default_elim"
       (str "Cannot find the elimination combinator " ++
@@ -546,7 +546,7 @@ let lookup_eliminator ind_sp s =
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-    try constr_of_reference (Nametab.locate (make_short_qualid id))
+    try constr_of_global (Nametab.locate (make_short_qualid id))
     with Not_found ->
       errorlabstrm "default_elim"
 	(str "Cannot find the elimination combinator " ++
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 3736419e24..34eb6d78de 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -101,7 +101,7 @@ let matches_core convert allow_partial_app pat c =
 
       | PVar v1, Var v2 when v1 = v2 -> sigma
 
-      | PRef ref, _ when constr_of_reference ref = cT -> sigma
+      | PRef ref, _ when constr_of_global ref = cT -> sigma
 
       | PRel n1, Rel n2 when n1 = n2 -> sigma
 
@@ -142,7 +142,7 @@ let matches_core convert allow_partial_app pat c =
 
       | PRef (ConstRef _ as ref), _ when convert <> None ->
 	  let (env,evars) = out_some convert in
-	  let c = constr_of_reference ref in
+	  let c = constr_of_global ref in
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bc6294d764..55fad22826 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -237,7 +237,7 @@ let make_dep_of_undep env (IndType (indf,realargs)) pj =
 (* Main pretyping function                                               *)
 
 let pretype_ref isevars env ref = 
-  let c = constr_of_reference ref in
+  let c = constr_of_global ref in
   make_judge c (Retyping.get_type_of env Evd.empty c)
 
 let pretype_sort = function
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4ac300827e..c30c0bd9f7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -933,7 +933,7 @@ let default_superauto g = superauto !default_search_depth [] [] g
 let interp_to_add gl locqid =
   let r = Nametab.global locqid in
   let id = id_of_global r in
-  (next_ident_away id (pf_ids_of_hyps gl), constr_of_reference r)
+  (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
 
 let gen_superauto nopt l a b gl =
   let n = match nopt with Some n -> n | None -> !default_search_depth in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bc91ddb3ec..7b595a0733 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1882,7 +1882,7 @@ let abstract_subproof name tac gls =
     let cd = Entries.DefinitionEntry const in
     let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
     let newenv = Global.env() in
-    constr_of_reference (ConstRef con)
+    constr_of_global (ConstRef con)
   in
   exact_no_check 
     (applist (lemme,