← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to plugins/xml/cic2acic.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/xml/cic2acic.ml
571
571
                   N.Anonymous
572
572
                  else
573
573
                   N.Name
574
 
                    (Nameops.next_name_away n (Termops.ids_of_context env))
 
574
                    (Namegen.next_name_away n (Termops.ids_of_context env))
575
575
              in
576
576
               Hashtbl.add ids_to_inner_sorts fresh_id''
577
577
                (string_of_sort innertype) ;
607
607
               match n with
608
608
                  N.Anonymous -> N.Anonymous
609
609
                | _ ->
610
 
                  N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
 
610
                  N.Name (Namegen.next_name_away n (Termops.ids_of_context env))
611
611
              in
612
612
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
613
613
               let sourcetype = CPropRetyping.get_type_of env evar_map s in
655
655
                 | N.Name id -> id
656
656
              in
657
657
              let n' =
658
 
               N.Name (Nameops.next_ident_away id (Termops.ids_of_context env))
 
658
               N.Name (Namegen.next_ident_away id (Termops.ids_of_context env))
659
659
              in
660
660
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
661
661
               let sourcesort =
771
771
                  (function
772
772
                      N.Anonymous -> Util.error "Anonymous fix function met"
773
773
                    | N.Name id as n ->
774
 
                       let res = N.Name (Nameops.next_name_away n !ids) in
 
774
                       let res = N.Name (Namegen.next_name_away n !ids) in
775
775
                        ids := id::!ids ;
776
776
                        res
777
777
                 ) f
805
805
                  (function
806
806
                      N.Anonymous -> Util.error "Anonymous fix function met"
807
807
                    | N.Name id as n ->
808
 
                       let res = N.Name (Nameops.next_name_away n !ids) in
 
808
                       let res = N.Name (Namegen.next_name_away n !ids) in
809
809
                        ids := id::!ids ;
810
810
                        res
811
811
                 ) f