From d8da8cb7b9af7df65f63af30bfa5775531426165 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 31 Mar 2003 11:57:52 +0000
Subject: factorisation des "constant" dans les contrib/* ( maintenant dans
 coqlib )

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 20 +++-----------------
 1 file changed, 3 insertions(+), 17 deletions(-)

(limited to 'tactics')

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 4468fd4d35..e397cd0cfe 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -47,23 +47,9 @@ type morphism =
 
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
-let constant dir s =
-  let dir = make_dirpath
-              (List.map id_of_string (List.rev ("Coq"::"Setoids"::dir))) in
-  let id = id_of_string s in
-    try 
-      Declare.global_reference_in_absolute_module dir id
-  with Not_found ->
-    anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id)))
-
-let global_constant dir s =
-  let dir = make_dirpath
-              (List.map id_of_string (List.rev ("Coq"::"Init"::dir))) in
-  let id = id_of_string s in
-    try 
-      Declare.global_reference_in_absolute_module dir id
-  with Not_found ->
-    anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id)))
+let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
+
+let global_constant dir s =Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s
 
 let current_constant id =
   try
-- 
cgit v1.2.3