diff options
| -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)) |