From 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 9 Nov 2009 18:05:13 +0000
Subject: A bit of cleaning around name generation + creation of dedicated file
 namegen.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/cic2acic.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/xml')

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 7706a3eb5..7f7bf5bf3 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -571,7 +571,7 @@ print_endline "PASSATO" ; flush stdout ;
                    N.Anonymous
                   else
                    N.Name
-                    (Nameops.next_name_away n (Termops.ids_of_context env))
+                    (Namegen.next_name_away n (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id''
                 (string_of_sort innertype) ;
@@ -607,7 +607,7 @@ print_endline "PASSATO" ; flush stdout ;
                match n with
                   N.Anonymous -> N.Anonymous
                 | _ ->
-                  N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
+                  N.Name (Namegen.next_name_away n (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcetype = CPropRetyping.get_type_of env evar_map s in
@@ -655,7 +655,7 @@ print_endline "PASSATO" ; flush stdout ;
                  | N.Name id -> id
               in
               let n' =
-               N.Name (Nameops.next_ident_away id (Termops.ids_of_context env))
+               N.Name (Namegen.next_ident_away id (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcesort =
@@ -771,7 +771,7 @@ print_endline "PASSATO" ; flush stdout ;
                   (function
                       N.Anonymous -> Util.error "Anonymous fix function met"
                     | N.Name id as n ->
-                       let res = N.Name (Nameops.next_name_away n !ids) in
+                       let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
                         res
                  ) f
@@ -805,7 +805,7 @@ print_endline "PASSATO" ; flush stdout ;
                   (function
                       N.Anonymous -> Util.error "Anonymous fix function met"
                     | N.Name id as n ->
-                       let res = N.Name (Nameops.next_name_away n !ids) in
+                       let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
                         res
                  ) f
-- 
cgit v1.2.3