diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-30 16:46:51 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-30 16:46:51 +0000 |
| commit | 2fe02b651f1977c6b9ada62c1f1457a437fa6090 (patch) | |
| tree | 9310e1db417f12efcc562e065222b1de5a03bf19 /tactics/tactics.ml | |
| parent | 8905764cd0373156f5eb3427fbb6ac99bf8d3560 (diff) | |
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
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 12bb61ad3..690f1f4f9 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 = |