From d599099f4a1b90ced74d3516530900c3e4c14944 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 23:47:32 +0000
Subject: Retrait du test d'existence "is_global" dans Intro ( fresh_id ) d

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 09abbe9157..28b9f36dc7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -238,19 +238,20 @@ let unfold_constr c =
 let next_global_ident_from id avoid = 
   let rec next_rec id =
     let id = next_ident_away_from id avoid in
-    if not (Declare.is_global id) then 
+(*    if not (Declare.is_global id) then *)
       id
-    else  
+(*    else  
       next_rec (lift_ident id)
-  in 
+*)  in 
   next_rec id
 
 let next_global_ident_away id avoid =
   let id  = next_ident_away id avoid in
-  if not (Declare.is_global id) then 
+(*  if not (Declare.is_global id) then *)
     id
-  else  
+(*  else  
     next_global_ident_from (lift_ident id) avoid
+*)
 
 let fresh_id avoid id gl =
   next_global_ident_away id (avoid@(pf_ids_of_hyps gl))
-- 
cgit v1.2.3