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

4 files changed, 9 insertions, 9 deletions

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