From d0a324eef4d35a87e300a2b660b26fdbe2043d92 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 May 2005 15:54:50 +0000
Subject: Adoption du nom canonique global_of_constr pour éviter confusion avec
 type reference

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml    | 4 ++--
 tactics/tactics.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ea7c62a1c3..0fda09a9aa 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -423,7 +423,7 @@ let add_hints local dbnames0 h =
       let f (n,c) =
 	let c = Constrintern.interp_constr sigma env c in
 	let n = match n with
-	  | None -> (*id_of_global (reference_of_constr c)*)
+	  | None -> (*id_of_global (global_of_constr c)*)
               id_of_string "<anonymous hint>"
 	  | Some n -> n in
 	(n,c) in
@@ -433,7 +433,7 @@ let add_hints local dbnames0 h =
       let f (n,c) = 
 	let c = Constrintern.interp_constr sigma env c in
 	let n = match n with
-	  | None -> (*id_of_global (reference_of_constr c)*)
+	  | None -> (*id_of_global (global_of_constr c)*)
               id_of_string "<anonymous hint>"
 	  | Some n -> n in
 	(n,c) in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 198a17bcd9..0216b3b659 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1465,7 +1465,7 @@ let compute_elim_signature elimt names_info =
     error_ind_scheme "the conclusion of";
   let indhd,indargs = decompose_app ind in
   let indt = 
-    try reference_of_constr indhd
+    try global_of_constr indhd
     with _ -> error "Cannot find the inductive type of the inductive schema" in
   let nparams = List.length indargs - nrealargs in
   let revparams, revhyps2 = chop_context nparams (List.rev hyps1) in
-- 
cgit v1.2.3