From 50da43eaa170cd051de690d7a396d56060c60e87 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Jun 2001 03:01:14 +0000
Subject: Backtrack vers comportement de la V6 pour eviter les globaux dans le
 nommage des variables

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1776 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c1a23755cc..886620bc95 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -258,7 +258,7 @@ let next_global_ident_away id avoid =
     next_global_ident_from (lift_ident id) avoid
 
 let fresh_id avoid id gl =
-  next_ident_away id (avoid@(pf_ids_of_hyps gl))
+  next_global_ident_away id (avoid@(pf_ids_of_hyps gl))
 
 let id_of_name_with_default s = function
   | Anonymous -> id_of_string s
-- 
cgit v1.2.3