From a3e7259781f462865f9d8c17c546b86eeffd7b3e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:53:41 +0000
Subject: Indépendance vis à vis de Declare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4379 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/pdb.ml    | 2 +-
 contrib/correctness/perror.ml | 2 +-
 contrib/correctness/pmisc.ml  | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 3aeb876ddb..46d86a3f6b 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -21,7 +21,7 @@ open Penv
 
 let cci_global id =
   try
-    Declare.global_reference id
+    global_reference id
   with
     _ -> raise Not_found
 
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 19b4db9928..18498377fb 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -66,7 +66,7 @@ let check_for_array loc id = function
 let is_constant_type s = function
     TypePure c ->
       let id = id_of_string s in
-      let c' = Declare.global_reference id in
+      let c' = Termops.global_reference id in
       Reductionops.is_conv (Global.env()) Evd.empty c c'
   | _ -> false 
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 60f7306ac5..ca7cee2e2e 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -170,7 +170,7 @@ let coq_false = mkConstruct ((bool_sp,0),2)
 
 let constant s =
   let id = id_of_string s in
-  Declare.global_reference id
+  Termops.global_reference id
 
 let connective_and = id_of_string "prog_bool_and"
 let connective_or  = id_of_string "prog_bool_or"
-- 
cgit v1.2.3