← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to plugins/funind/rawterm_to_relation.ml

  • Committer: herbelin
  • Date: 2009-11-09 18:05:13 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12485
A bit of cleaning around name generation + creation of dedicated file namegen.ml

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/funind/rawterm_to_relation.ml
138
138
  let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
139
139
    match na with
140
140
       | Name id when List.mem id avoid ->
141
 
           let new_id = Nameops.next_ident_away id avoid in
 
141
           let new_id = Namegen.next_ident_away id avoid in
142
142
           Name new_id,Idmap.add id new_id mapping,new_id::avoid
143
143
       | _ -> na,mapping,avoid
144
144
  in
168
168
            if need_convert_id avoid id
169
169
            then
170
170
              let new_avoid =  id::avoid in
171
 
              let new_id = Nameops.next_ident_away id new_avoid in
 
171
              let new_id = Namegen.next_ident_away id new_avoid in
172
172
              let new_avoid' = new_id :: new_avoid in
173
173
              let mapping = Idmap.add id new_id Idmap.empty in
174
174
              let new_ctxt' = change_vars_in_binder mapping ctxt' in
550
550
                  match n with
551
551
                    | Name id when List.exists (is_free_in id) args ->
552
552
                        (* need to alpha-convert the name *)
553
 
                        let new_id = Nameops.next_ident_away id avoid in
 
553
                        let new_id = Namegen.next_ident_away id avoid in
554
554
                        let new_avoid = id:: avoid in
555
555
                        let new_b =
556
556
                          replace_var_by_term