From 5e0f9cb6eecc1c02566278ede0cb86ef68a03662 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 12 Sep 2003 14:47:18 +0000
Subject: Indépendance vis à vis de Declare
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1b9f86023..41dce0fef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -21,7 +21,6 @@ open Inductiveops
 open Reductionops
 open Environ
 open Libnames
-open Declare
 open Evd
 open Pfedit
 open Tacred
@@ -229,12 +228,13 @@ let unfold_constr = function
 (*******************************************)
 
 let is_section_variable id =
-  try let _ = Declare.find_section_variable id in true with Not_found -> false
+  try let _ = Sign.lookup_named id (Global.named_context()) in true
+  with Not_found -> false
 
 let next_global_ident_from id avoid = 
   let rec next_rec id =
     let id = next_ident_away_from id avoid in
-    if is_section_variable id || not (Declare.is_global id) then
+    if is_section_variable id || not (is_global id) then
       id
     else  
       next_rec (lift_ident id)
@@ -243,7 +243,7 @@ let next_global_ident_from id avoid =
 
 let next_global_ident_away id avoid =
   let id  = next_ident_away id avoid in
-  if is_section_variable id || not (Declare.is_global id) then
+  if is_section_variable id || not (is_global id) then
     id
   else  
     next_global_ident_from (lift_ident id) avoid
-- 
cgit v1.2.3