diff options
| author | herbelin | 2000-12-25 23:47:32 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-25 23:47:32 +0000 |
| commit | d599099f4a1b90ced74d3516530900c3e4c14944 (patch) | |
| tree | 97368ab1cc165b09185a693b06ae59f7d86e2728 | |
| parent | 2e03ae95b48638c01d66ecced32a4f5ae24a3e6e (diff) | |
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
| -rw-r--r-- | tactics/tactics.ml | 11 |
1 files 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)) |