From 2fe02b651f1977c6b9ada62c1f1457a437fa6090 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Jul 2002 16:46:51 +0000
Subject: Branchement de Assert, Pose et LetTac sur l'algo de création de noms
 frais de Intro

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 12bb61ad3e..690f1f4f9e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -527,7 +527,7 @@ let true_cut idopt c gl =
 	  match idopt with
 	  | None -> 
               let d = match s with Prop _ -> "H" | Type _ -> "X" in
-              next_name_away_with_default d Anonymous (pf_ids_of_hyps gl)
+              fresh_id [] (id_of_string d) gl
 	  | Some id -> id
 	in
 	internal_cut id c gl
@@ -695,11 +695,9 @@ let letin_abstract id c occs gl =
 
 let letin_tac with_eq name c occs gl =
   let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
-  let env = pf_env gl in
-  let used_ids = ids_of_context env in
   let id =
-    if name = Anonymous then next_ident_away x used_ids else
-      if not (mem_named_context x (named_context env)) then x else
+    if name = Anonymous then fresh_id [] x gl else
+      if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared") in
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
   let ctxt =
-- 
cgit v1.2.3